%\documentclass[a4paper,10pt]{article}
\documentclass[envcountsect,envcountsame,runningheads,a4paper,orivec]{llncs} 
% \documentclass[runningheads,a4paper]{llncs}


%\usepackage[utf8]{inputenc} \usepackage{times}
\usepackage[T1]{fontenc} 
\usepackage{tgtermes}

\usepackage[english]{babel}
\usepackage{xspace}
\usepackage{float}
\usepackage{mathpartir}

\usepackage{amstext, amssymb, amsfonts, amsmath}
\usepackage{latexsym}
\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{enumerate}

\usepackage{color}
\usepackage{url}
\usepackage{hyperref}
\usepackage{proof}

\usepackage{macron}
\usepackage{typecasemacro}



\newenvironment{rcases}
  {\left\lbrace\begin{aligned}}
  {\end{aligned}\right\rbrace}
  
\usepackage{lineno}

\newtheorem{newnotation}[theorem]{Notation}



%opening
\title{
%An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems\thanks{DRAFT - Revision of \today}
An Event-Based Approach to Runtime Adaptation in Communication-Centric Systems
%An Event-Based Architecture for Runtime Adaptation in Communication-Centric Systems
}
%\titlerunning{Event-Based Adaptation in Communication-Centric Systems (\today)}
\titlerunning{Event-Based Runtime Adaptation in Communication-Centric Systems}
\author{Cinzia Di Giusto$^{1}$ \and Jorge A. P\'{e}rez$^{2}$}
\authorrunning{Cinzia Di Giusto and Jorge A. P\'{e}rez}
\institute{%Universite d'Evry 
$^{1}$ Universit\'{e} d'Evry %- Val d'Essonne, Laboratoire IBISC, Evry
\quad $^{2}$ %Johann Bernoulli Institute for Mathematics and Computer Science, 
University of Groningen}

\widowpenalty=0
\clubpenalty=0

\begin{document}

\maketitle



\vspace{-4mm}     
\begin{abstract}
%%Modern distributed software systems are \emph{communication-centric}: 
%%built as assemblies of software artifacts, 
%%these systems rely on consistent dialogues among such artifacts. 
%%Ensuring conformance of these dialogues to prescribed protocols is thus key to correctness.
%% As  systems become more complex, correctness analyses must unavoidably 
%% account for issues not strictly tied to communication but that influence overall   behavior.
%% This paper deals with one of such issues,
%% \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
%%Concretely, we are interested in integrating mechanisms for runtime adaptation into \emph{session types} for structured communications.
%%We offer two main contributions.
%%First, by  relying on selected features from  
%%the eventful session framework by Kouzapas et al, 
%%we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
%%Our approach enables us to  define rich forms of adaptation, 
%%even for processes with active running sessions.
%%Second,
%%we propose a simple architecture for communication-centric systems with runtime adaptation. 
%%By formalizing \emph{compartmentalized} communications, 
%%our architecture offers  an alternative for organizing session-based systems and services.
%====
%Modern distributed  systems are \emph{communication-centric}: 
%built as assemblies of software artifacts, 
%these systems rely on consistent dialogues among such artifacts. 
% As systems become more complex, the analysis of communication correctness must unavoidably 
% account for issues not strictly tied to communication but that influence overall   behavior.
% This paper addresses  one of such issues,
% \emph{runtime adaptation},  here understood as the dynamic update of the behavior of part of the system.
%Concretely, we are interested in integrating mechanisms for runtime adaptation into \emph{session types} for structured communications.
%We offer two main contributions.
%First, by  relying on selected features from the eventful session framework by Kouzapas et al, 
%we propose an \emph{event-based}  approach to runtime adaptation of session typed processes.
%Our approach improves prior works by 
%enabling rich forms of adaptation, 
%even for processes with active sessions.
%Second,
%we propose a 
%model of \emph{compartmentalized} communication-centric systems with runtime adaptation. 
%This model offers  an alternative for organizing session-based systems and services and their associated adaptation 
%mechanisms.
%====
This paper addresses the enhancement of process frameworks based on \emph{session types} %for structured communications 
with mechanisms for \emph{runtime adaptation}---here understood as the dynamic update of the behavior of part of the system.
We propose an \emph{event-based} approach: 
% to runtime adaptation of session typed processes.
%In our framework, 
adaptation requests are assimilated to \emph{events}
which may trigger runtime adaptation routines 
%with appropriate types.
which depend on the current protocol state. % at a given time
%First, by  relying on %selected 
%constructs from the eventful session framework by Kouzapas et al., 
Such requests may come from the system or from its environment, and are treated uniformly.
%By keeping detailed descriptions of the protocol state, 
Our approach %improves prior works by 
enables rich forms of adaptation, even for processes with active sessions.
An associated type system ensures communication safety and consistent updates.
We also propose a high-level
model of \emph{compartmentalized} communication which integrates
session-based specifications and their runtime adaptation mechanisms.
%\vspace{-3mm}    
\end{abstract}
%
%\section{Suggestions}
%%The abstract can be much shorter and more general. 
%
%Mention the well-known work on exceptions for binary session types, and other session disciplines with buffers/queues~\cite{DBLP:journals/jfp/GayV10}.
%
%Before giving technical details, it would be very useful to give a concrete example for configurations/networks, and their evolution.
%The example could illustrate records, memories, etc. 


% \linenumbers

\section{Introduction}
\noindent{\textit{\textbf{Context.}}}
Modern software 
systems are built as assemblies of heterogeneous  ar\-ti\-facts
which must interact following predefined protocols.
Correctness in these \emph{com\-mu\-ni\-ca\-tion-centric} systems
largely depends on ensuring that such dialogues are consistent.
\emph{Session-based concurrency} is a type-based approach to 
ensure conformance of dialogues to prescribed protocols:
 dialogues are organized into %basic 
 units called \emph{sessions}; interaction patterns are abstracted as \emph{session types}~\cite{DBLP:conf/esop/HondaVK98}, 
against which specifications may be checked. %\looseness=-1

As communication-centric systems %typically %open, and  
operate on open, highly dynamic infrastructures, 
\emph{runtime adaptation} appears as a crucial feature to ensure continued system operation.
We understand runtime adaptation as the dynamic modification of (the behavior of) the system in response to an exceptional  \emph{event}, not necessarily catastrophic. 
As such, 
protocol conformance and 
dynamic reconfiguration are intertwined concerns:
although 
the specification of runtime adaptation is 
not strictly tied to that of structured protocols, 
steps of dynamic reconfiguration have a direct influence in a system's interactive behavior.

We address the integration of mechanisms for runtime adaptation
into %a model of 
session-based concurrency.
As a first answer to this challenge, in previous work~\cite{GiustoP14} we
proposed the first typeful integration of  basic adaptation mechanisms into a session typed framework.
Here we propose %a framework in which  
adaptation mechanisms which depend on the protocol state,
thus extending their applicability and expressiveness.
%thus enabling the specification of more fine-grained adaptation strategies.
As a distinctive feature, we advocate an \emph{event-based} approach:
by combining constructs for \emph{non-blocking event detection} and \emph{dynamic type inspection} (as put forward by Kouzapas et al.~\cite{KouzapasJ13,Kouzapas12}), adaptation requests, either internal or external to the session protocols, can be naturally assimilated to events.

%\paragraph{Our Approach, By Example.}
\paragraph{\textbf{A Running Example.}}
%We describe our approach and motivate our contributions using a simple example.
Consider 
%the %structured 
%interaction of 
a buyer \pt{B} and a seller \pt{S} which follow the protocol given next. % following the protocol.
First, \pt{B} sends to \pt{S} the name of an item and \pt{S} replies back with its price. 
Then, depending on this amount, \pt{B} may either add the item to its shopping cart or cancel the transaction. 
In the latter case the protocol ends.
In the former case \pt{B} must further choose its paying method. % and the transaction ends.
From \pt{B}'s perspective, this protocol may be described by 
the session type $\ST = \,\,!\mathsf{str}.\,?\mathsf{int}.\,\ST_{\mathtt{pay}}$, where 
$\mathsf{str}$ and $\mathsf{int}$ are base types and
$\ST_{\mathtt{pay}}$ is defined as
\begin{equation*}
\ST_{\mathtt{pay}} \,=\,\oplus\{\mathtt{addItem}:\, \oplus\{\mathtt{ccard}:\, \ST_\mathtt{cc} \,,\, \mathtt{payp}:\, \ST_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \}  
\end{equation*}
%In the syntax of session types, 
Above 
$!$ and $?$ stand for output and input, %respectively, 
$\oplus$ denotes a labeled internal choice, 
and 
$\tend$ stands for the completed protocol. 
%In $\ST_{\mathtt{pay}}$, 
%Session 
Types 
%we write 
$\ST_\mathtt{cc}$ and $\ST_\mathtt{pp}$ denote the behavior of each payment method.
Following~$\ST$, \pt{B} may be implemented as a  $\pi$-calculus process. 
Below we give a particular implementation, in which \pt{B} buys a book only when its price is less than \$50:
\begin{eqnarray*}
P^{50}_x & = & \outC{x}{\mathsf{book}}.\inC{x}{a}.\ifte{a < 50}{\select{x}{\mathtt{addItem}};\select{x}{\mathtt{ccard}};P_x^{\mathsf{c}}}{\select{x}{\mathtt{cancel}};\mathbf{0}} 
%Q_y & = & \inC{y}{i}.\outC{y}{price(i)}.\branch{y}{\mathtt{addItem} : \branch{y}{\mathtt{ccard}: Q_y^{\mathtt{c}} \alte \mathtt{ppal}: Q_y^{\mathsf{p}}} \alte \mathtt{cancel}: \mathbf{0}} 
\end{eqnarray*}
where $P_x^{\mathsf{c}}$ implements $\ST_{\mathtt{cc}}$.
To ensure protocol compatibility and absence of  communication errors, 
the session type for \pt{S}, denoted $\STT$, 
should be \emph{dual} to $\ST$. %; this is written $\ST \cdual \STT$.
%Intuitively, duality says that 
That is,
every action from \pt{B} is matched by a complementary action from \pt{S}.
This way, $\STT = \,\,?\mathsf{item}.\,!\mathsf{price}.\,\STT_{\mathtt{pay}}$, where
type $\STT_{\mathtt{pay}}$ and a particular implementation for \pt{S} are as follows:
\begin{eqnarray*}
\STT_{\mathtt{pay}} & = & \&\{\mathtt{addItem}:\, \&\{\mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \}  \\
Q_y & = & \inC{y}{i}.\outC{y}{price(i)}.\branch{y}{\mathtt{addItem} : \branch{y}{\mathtt{ccard}: Q_y^{\mathtt{c}} \alte \mathtt{ppal}: Q_y^{\mathsf{p}}} \alte \mathtt{cancel}: \mathbf{0}} 
\end{eqnarray*}
Above, 
$\&$ denotes the type for external choice. Also, processes
$Q_y^{\mathsf{c}}$ and $Q_y^{\mathsf{p}}$ implement 
$\STT_{\mathtt{cc}}$ and $\STT_{\mathtt{pp}}$ (the duals of $\ST_{\mathtt{cc}}$ and $\ST_{\mathtt{pp}}$).
This way, writing $\nopenr{u}{x{:}\ST}.P$ (resp. $\nopena{u}{x{:}\ST}.P$)
to denote a session request (resp. acceptance) on name $u$, 
the system may be specified as 
\begin{equation*}
 \nopenr{u}{x{:}\ST}.P^{50}_x \para \nopena{u}{y{:}\STT}.Q_y 
\end{equation*}
Then, upon synchronization on $u$, a pair of \emph{session channels}, one for each partner, 
is generated at runtime. They can be used to execute the protocols described by $\ST$ and $\STT$. 
\paragraph{\textbf{Our Approach To Adaptation.}}
Our process language extends a standard session $\pi$-calculi with \emph{locations}, 
\emph{located processes}, and \emph{update processes}~\cite{BGPZFMOODS}.
We use \emph{locations} as explicit delimiters for runtime adaptation: 
these are transparent, possibly nested computation sites.
Given a location $\locf{loc}$  and a process $P$, 
the \emph{located process} $\scomponent{\locf{loc}}{P}$ denotes the fact that $P$ resides in \locf{loc} (or, alternatively, that $P$ has scope $\locf{loc}$).
This way, e.g., 
process
\begin{equation*}
W  =   \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST}.P^{50}_x} \para  \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT}.Q_y} \,} 
\end{equation*}
represents an explicitly distributed variant of the buyer-seller scenario:
the partners now reside in locations \locf{buyer} and \locf{seller}; location \locf{sys} encloses the whole system.
%We use locations as explicit delimiters for runtime adaptation steps: 
An \emph{update process}, denoted $\nadapt{\locf{loc}}{R}$, informally says that the behavior currently enclosed by 
\locf{loc}
should be replaced according to $R$.
%This way, 
%to define adaptation %at the level of  
%%for endpoints 
%we may extend $W$ with update processes 
%$\nadapt{\locf{buyer}}{R_b}$ and $\nadapt{\locf{seller}}{R_r}$.
Since a location  may enclose 
one or more %interacting parties, 
session channels,
update processes allow for flexible specifications of adaptation routines. %than one session. 
This way, e.g., one may specify an update on \locf{buyer} that does not involve \locf{seller} (and vice versa); 
also,  %by defining an appropriate $\nadapt{\locf{buyer}}{R_b}$; 
given an $R_s$ that accounts for both buyer and seller behaviors, 
a system-level adaptation could be defined by adding process  $\nadapt{\locf{sys}}{R_s}$ 
in parallel to $W$. 

The 
integration of runtime adaptation into sessions %-based concurrency
is delicate, and involves
defining \emph{when}
an adaptation step should be triggered and \emph{what} should be the resulting state of the system. % after  such a step.
To rule out careless adaptation steps which jeopardize established protocols, % (or even discard active endpoints), 
communication and adaptation actions should be harmonized. 
In previous work~\cite{GiustoP14}
we proposed 
%a solution that consists in 
admitting adaptation actions only when  locations do not enclose running sessions. 
This means, e.g., that an upgrade of the payment protocols in \locf{seller} is only enabled
%only take place only 
when the seller process is 
idle.
%not interacting with a buyer.
This solution is \emph{asymmetric}, %in the sense that 
for
it privileges communication over adaptation. 
However, it is easy to imagine that actual protocols
could benefit from more symmetric approaches.
Returning to the example, 
an % system-level 
adaptation which adds a new payment method to the seller
(and extends the buyer's interface)
would 
%come in handy for active 
be useful for running 
sessions in which the buyer has not yet selected how to pay.

In the framework presented here we admit the adaptation of locations with running sessions.
We propose update processes 
$\nadapt{\locf{loc}}{R}$ in which $R$ is able to 
%with the ability of 
dynamically check
the current state of the
session protocols running in  \locf{loc}.
In their simplest form, our update processes 
concern only one protocol/session and are of the shape
%are written
\begin{equation*}
 {\nadaptbig{\locf{loc}}{\mycase{{x}}{{x_{}^{}{:}\STT_{}^{i}}}{R_i}{i \in I}}}  
\end{equation*}
where
$I$ is a finite index set, 
each 
 $\STT^i$ is a session type, and 
$x$ is a free variable in 
each \emph{alternative} $R_i$.
This construct has the following intuitive semantics.
Consider a located process 
$\scomponentbig{\locf{loc}}{ Q} $
such that $Q$ implements a single session of
type $\ST$ along a channel $\cha^p$.
There are two possibilities for the interaction between this located process and the update process above.
If there is an alternative $j \in I$  such that 
session types $\ST$ and $\STT^j$ ``match''
then there is a reduction step to process 
$\scomponentbig{\locf{loc}}{ R_j\subst{\cha^p}{x}}$. 
Otherwise, if no $\STT^j$ validates a match, then the 
reduction reads to 
$\scomponentbig{\locf{loc}}{ Q}$, i.e., the behavior of \locf{loc} is kept unchanged. 

In general, update processes may define adaptation for locations enclosing more than one session channel. 
In the distributed buyer-seller example, %For instance, 
the process below defines
a runtime update which depends on the current protocol state at location $\locf{sys}$:
%\begin{equation}
%R_{xy} = {\nadaptbig{\locf{sys}}{\mycase{{x,y}}{x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}}{\scomponent{\locf{buyer}}{ P'_x} \para  \scomponent{\locf{seller}}{ Q'_y}}{}}} \label{eq:intro}
%\end{equation}
\begin{equation}
R_{xy} = {\nadaptbigg{\locf{sys}}{
\mathsf{case\,}x,y\, \mathsf{of}
\begin{rcases}
(x{:}\ST \,;\, y{:}\STT) & :  \scomponent{\locf{buyer}}{ P^{100}_x} \para  \scomponent{\locf{seller}}{Q_y} \\
(x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}) & :  \scomponent{\locf{buyer}}{ P^*_x} \para  \scomponent{\locf{seller}}{ Q^*_y}
\end{rcases}
}} \label{eq:intro}
\end{equation}
$R_{xy} $ is an update process with only one alternative. 
%There are two possibilities for update which depend on the protocol state.
If the protocol has just been established (i.e., current types are $\ST$ and $\STT$) then only the buyer is updated---she will now be able to spend up to \$100.
If both item and price information have been already exchanged then new implementations $P^*_x$ and $Q^*_y$, tailored to types $\ST_{\mathtt{pay}}$ and $\STT_{\mathtt{pay}}$, are deployed.

Update processes rely on the protocol state at a given location to assess the suitability of adaptation routines. 
%adaptation actions may safely take place on locations enclosing open sessions. 
Our semantics for update relies on 
(a)~\emph{monitors} which store  the  current type for each running session; and 
(b)~a type-directed test on the monitors
%subtyping to test the state of a set of sessions 
enclosed in a given location. 
This test %  as a %actually corresponds to  
generalizes the $\mathtt{typecase}$ construct in~\cite{Kouzapas12}.

%\paragraph{\textbf{Event-Based Adaptation.}}
While expressive, 
%Defined at the level of locations, 
our typeful update processes %thus offer a flexible and expressive mechanism for runtime adaptation.
by themselves %, however, these processes 
do not specify \emph{when} adaptation should be available. 
Even though update processes could be embedded within session communication prefixes (thus creating casual dependencies between communication and adaptation),
such a specification style would only allow to handle the class of exceptional conditions which can be fully characterized in advance.
Other classes of exceptional conditions, in particular contextual and/or unsolicited runtime conditions, are much harder to express by interleaving update processes 
within structured protocols.

%Indeed, since update processes are consumed after every test (i.e., they are not persistent), it is not clear how they should occur in specifications nor how they should be triggered. 

To offer a uniform solution to this issue, 
%the constructs of 
our process model follows an \emph{event-based} approach
to trigger updates.
%In order  %, we rely on \emph{events}.
We endow each location with a \emph{queue} of adaptation requests; 
such requests  
%these requests 
%are simply treated as messages and
may be internal or external to the location.
In our example, an external request could be, e.g., 
%a signal from the infrastructure on which both partners are deployed, or 
a warning message from the buyer's bank indicating that an exchange with the bank is required before committing to the purchase with seller. 

Location queues  are independent from session behavior.
Their identity is visible to processes;
they are intended as interfaces with other process and the environment. 
%This way, e.g., the queue of location \locf{seller} becomes the only way in which its surrounding context may only influence the communication behavior. 
To issue an adaptation request $r$, our process syntax includes  \emph{adaptation signals}, written $\outC{\locf{loc}}{r}$.
%where $r$ stands for an adaptation request.
Orthogonal to sessions, these signals are expected to occur within communication prefixes. 
% processes such as $P_x$ and $Q_y$ may issue adaptation requests.
Then, using the \emph{arrival predicate} of~\cite{Kouzapas12}, 
here denoted $\arrive{\locf{loc}, r}$, 
we may 
detect the presence of %message 
$r$ in the queue of %location 
\locf{loc}.
This way, e.g., 
%As an illustration of our event-based constructs for adaptation, 
the  process below combines update process $R_{xy}$ in \eqref{eq:intro} with recursion, conditionals and arrival predicates:
\begin{equation}
R^*_{xy} = \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{R_{xy}}{\rv{X}}
\end{equation}
Thus, process $R^*_{xy}$ continuously checks if an \emph{external}  request $\mathtt{upd}_E$ has been queued for
location \locf{sys}. As soon as such a request is detected update process $R_{xy}$ will be triggered.
%Using a so-called \emph{adaptation signal}, written $\outC{\locf{sys}}{r}$,
% processes such as $P_x$ and $Q_y$ may issue adaptation requests. 
% These signals are meant to occur as prefixes within communication structures.

Summing up, our process model handles eventful runtime adaptation 
by extending a standard session $\pi$-calculus with located and update processes, arrive predicates,  monitors, adaptation signals, and location queues. 


In the final part of the paper, we investigate 
how to rationalize process specifications 
of structured communications with runtime adaptation.
We outline a \emph{compartmentalized} model for communication-centric applications
which defines
modular units of communication and runtime adaptation.
%, and enforces the separation between communication behavior, event-related elements (e.g., queues), and adaptation constructs. 
%It can be seen as a simple but compelling illustration of 
This model illustrates
(a)~how our language can be used to reason about at higher levels of abstraction, and (b)~how to define interaction between constructs for communication and adaptation while enforcing formal and conceptual separations between them. 
Furthermore, our compartmentalized model suggests a basis for extending our developments to cover multiparty communications.
%We discuss the syntax and semantics for specifications of the compartmentalized model, and argue that the session type system for ``plain'' processes scales to compartmentalized processes. 




% The coupling of update processes and adaptation queues 
% gives us a rich framework
% for specifying session communication with  runtime adaptation mechanisms. % (see~\S\,\ref{s:evadap}).
% In our example, we may use (i) to endow locations \locf{ser} and \locf{cli} with  queues in which
% internal and external adaptation requests are collected; the message detector could define a different update process in each case. 
% Using (ii), we may specify adaptation steps which are triggered depending on the current state of the session between the bank and the client; for instance, we may decide to adapt the bank server if the $b$alance option has been selected.
%An associated type system %, developed in~\S\,\ref{s:types}, 
%ensures 
% communication safety and consistency for well-typed session processes.
%To the best of our knowledge, eventful session constructs have not been used for specifying runtime adaptation concerns; the framework we present here appears to be an  application of the event-based approach not previously identified.


\paragraph{\textbf{Main Contributions and Organization.}}
We summarize the contributions of the paper:
\vspace{-2mm}
\begin{enumerate}[-]
\item An event-based process model of session communications with typeful constructs for event-based runtime adaptation (\S\,\ref{s:evadap}).
\item A session type system for processes which 
ensures \emph{safety} (i.e., absence of communication errors) and 
\emph{consistency}, which intuitively guarantees that update steps do not jeopardize established session protocols  (\S\,\ref{s:types}).
 %retains a usual session type syntax and ensures safety and consistency for well-typed processes 



\item A compartmentalized process model which sheds light on the conceptual organization
for models of structured communication with runtime adaptation~(\S\,\ref{s:arch}).
\end{enumerate}
%The rest of the paper is structured as follows.
%In \S\,\ref{s:evadap} we present the process model for structured communication and enhanced runtime adaptation. 
%%Such mechanisms are illustrated in \S\,\ref{s:examp}, where we revisit the client-server scenario discussed above.
%In~\S\,\ref{s:types} we present the session  type system and state its main properties.
%The {compartmentalized} model for com\-muni\-cation-centric applications is presented in \S\,\ref{s:arch}.
At the end, we discuss related works and some concluding remarks (\S\,\ref{s:concl}).
The appendix collects 
%additional material, including 
%an example and 
omitted definitions and proofs. % are omitted.


%\subsection{Another Example}
%
%Consider a scenario in which two buyers $\mathtt{B1}$ and $\mathtt{B2}$ coordinate to buy an book from seller $\mathtt{S}$. 
%In the following protocol participant $\mathtt{B2}$ acts as a mediator between $\mathtt{S}$ and $\mathtt{B1}$:
%\begin{enumerate}
%\item $\mathtt{B1}$ opens a session with $\mathtt{B2}$ and uses it to send a book title (in Italian) that she would like to buy from a foreign seller she cannot communicate with.
%\item Upon reception of the title, $\mathtt{B2}$ opens a session with $\mathtt{S}$ and uses that session to send a Spanish translation of the title sent by $\mathtt{B2}$.
%\item $\mathtt{S}$ sends to $\mathtt{B2}$ the price of the book that $\mathtt{B1}$ wishes to buy. The currency of $\mathtt{S}$ is COP.
%\item After converting the price sent by $\mathtt{S}$ to Euro (the currency of $\mathtt{B1}$), $\mathtt{B2}$ sends to $\mathtt{B1}$ the amount of money that she should contribute with for buying the book. 
%\item Upon reception of the price in Euros, $\mathtt{B1}$ may decide to either (a) continue with the purchase or to (b) quit the transaction.
%\end{enumerate}
%The protocol comes with the following exceptional events:
%\begin{enumerate}[1.]
%\item Depending on the currency rates Euro-COP the quote that $\mathtt{B2}$ sends to $\mathtt{B1}$ may be too high for her. 
%In that case, $\mathtt{B2}$ triggers an adaptation request %for session $\ST_1$ 
%in order to include additional coordination with $\mathtt{B1}$.
%\item In case of technical issues on the platform in which $\mathtt{S}$ is deployed (communicated by an external monitor), the service must be relocated to an alternative platform in which the remainder of 
%%session $\ST_2$ 
%the protocol
%will be carried out.
%\item The interaction between $\mathtt{B2}$ and $\mathtt{S}$ may be randomly selected for feedback purposes. 
%%Session $\ST_2$ must  be adapted 
%Their protocol must be extended with  
%additional exchanges between $\mathtt{B2}$ and $\mathtt{S}$. Such exchanges, however, must only occur if $\mathtt{B2}$ has already decided to purchase the book.
%\end{enumerate}
%
%We may represent this scenario with two interleaved sessions: one between $\mathtt{B1}$ and $\mathtt{B2}$, and another one between $\mathtt{B2}$ and $\mathtt{S}$. These two sessions, seen from the perspective of $\mathtt{B2}$, may be expressed as session types $\ST_1$ and $\ST_2$, respectively:
%\begin{eqnarray*}
%\ST_1 & = & ?\mathsf{titleIT}.\,!\mathsf{quoteEU}.\,\oplus\{\mathtt{buy}:~ !\mathsf{ok}.\epsilon \, , \, \mathtt{leave}:~ !\mathsf{ko}.\epsilon \} \\
%\ST_2 & = & !\mathsf{titleES}.\,?\mathsf{priceCOP}.\,\oplus\{\mathtt{proceed}:~ !\mathsf{address}.\,!\mathsf{account}.\,\epsilon \, , \, \mathtt{quit}:~ !\mathsf{bye}.\epsilon \}
%\end{eqnarray*}




\section{The Process Model: Syntax and Semantics}\label{s:evadap}
%ADD POINTERS TO TYPES (duality, subtyping)


\begin{table}[t!]
$$
\begin{array}{lrlr}
%u & ::=  &   x, y  \sepr a, b & \text{names}	\\
% k & ::=  &   x, y \sepr \cha^{+}, \cha^{-} & \text{channels}	\\
%d & ::= & a, b  \,\sepr \cha^{+}, \cha^{-} & \text{identifiers} \\
%v & ::= & \mathtt{true}, \mathtt{false} \sepr a, b  \sepr \cha^{+}, \cha^{-} & \text{values} \\
%r	&::= &  \mathtt{upd}_I \sepr \mathtt{upd}_E \sepr\mathtt{upg} \sepr \cdots &\text{adaptation messages} \\
e & ::= & v \sepr x, y, z  \sepr k = k \sepr a = a & \text{expressions}  \\
%  & \sepr & \arrive{u}  \sepr \arrive{k} \sepr \arrive{k,h} & \text{arrive predicates (usual)}\\ 
  & \sepr & \arrive{\locf{loc}, r} & \text{arrive predicate} \\ 
P & ::=  &   \nopenr{u}{x:\ST}.P  ~~\sepr~~ \nopena{u}{x:\ST}.P  ~~\sepr~~\close{k}.P& \text{session request / acceptance / closure}	 \\
%	& \sepr &   \nopena{u}{x:\ST}.P  & \text{session acceptance}	\vspace{0.5mm} \\
	& \sepr &  \outC{k}{e}.P ~~~~\sepr~~ \inC{k}{x}.P  & \text{data output /input } \\
  %	&\sepr &    \inC{k}{x}.P  & \text{data input} \vspace{0.5mm} \\
	&\sepr&   \select{k}{n};P ~~\sepr~~  \branch{k}{n_i{:}P_i}_{i \in I} & \text{selection / branching} \\
%    &\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching} \vspace{0.5mm}\\
%		&\sepr&   \close{k}.P & \text{close session}	 \vspace{0.5mm}\\
    &\sepr&   \mu \rv{X}.P ~\,\sepr~~ \rv{X} & \text{recursion / rec. variable}  \\
%	& \sepr &   \rv{X}& \text{recursion variable}  \vspace{0.5mm}\\
  	& \sepr &   P \para  P  ~~\sepr~~   \mathbf{0}  & \text{parallel composition / inaction } \\	 
	&\sepr&   \restr{\cha}{P} ~\sepr~~ \restr{u}{P}  & \text{channel / name hiding}	\\
		  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional} \\
%	&\sepr&   \restr{a}{P}  & \text{name hiding}	\vspace{0.5mm} \\
%	&\sepr&   \mathbf{0}  & \text{inaction} \vspace{1.5mm} \\
	&\sepr&   \que{k}{\ST}  & \text{session monitor}  \\ 
		&\sepr&  \scomponent{\locf{loc}}{P}  & \text{located process}  \\
%	&\sepr&  \nadapt{l}{P} & \text{update process}\\
	&\sepr&  \nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}} \quad& \text{typeful update process} \\
	&\sepr&   \outC{\locf{loc}}{r} \sepr \que{\locf{loc}}{\til{r}} & \text{adaptation signal / queue} %\vspace{0.5mm} \\
	%&\sepr&   \que{\locf{loc}}{\til{r}}  & \text{queue for locations} 
%p	&::= &  + \sepr - &\text{channel polarities} \\
%h	&::= &  v \sepr n &\text{messages}  
%    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Process Syntax. %Session Processes with Runtime Adaptation: Syntax.
Above, annotation $\ST$ denotes a session type (cf. Def.~\ref{d:types})
} \label{tab:syntax}
\vspace{-7mm}
\end{table}


%TO DO: mention abbreviations (branching), notation for labels and locations, and close process, annotations for service requests, location messages.

%Our process language of sessions with runtime adaptation
%%In a nutshell, it which 
%combines the synchronous $\pi$-calculus 
%that we have considered in~\cite{DBLP:conf/sac/GiustoP13} with constructs from the eventful session framework in~\cite{Kouzapas12}. 
%%We  also give an operational semantics for processes \\
%%, and illustrate its use with a simple example. \\

%\noindent{\bf Syntax.~}
\paragraph{\textbf{Syntax.}}
We consider the following 
base sets: 
\emph{names}, ranged over by $u, a, b \ldots$; 
\emph{(session) channels}, ranged over by $k, \cha^p, \ldots$, with \emph{polarity} $p \in \{+,-\}$;
\emph{labels}, ranged over by $n, n', \ldots$; 
and \emph{variables}, ranged over by $x, y, \ldots$.
We use $r$ to range over \emph{adaptation messages}: two instances are 
$\mathtt{upd}_I$ and $\mathtt{upd}_E$, denoting internal and external requests, resp.
We also use $\,\til{\cdot}\,$ to denote finite sequences  of  entities. Thus, e.g., $\til{x}$ stands for a sequence of variables $x_1, \ldots, x_n$.

Table~\ref{tab:syntax} reports the syntax of expressions and processes.
Processes include usual constructs for intra-session input/output and labeled choice. 
Common forms of recursion, parallel composition, conditionals, and %name\-/\-chan\-nel 
restriction are also included.
As %hinted at above, 
motivated in the Introduction,
constructs for session establishment (request and accept)
rely on annotations with a session type $\ST$ and on \emph{duality}, denoted $\cdual$; see~\S\,\ref{s:types}.
We also have a prefix for closing a session, inherited from~\cite{GiustoP14}, useful to structure specifications. %Also, the process syntax includes 
%Binding is as follows: 
%the channel 
Variable $x$ is bound in processes 
$\nopenr{u}{x{:}\ST}.P$, $\nopena{u}{x{:}\ST}.P$, and 
%$x$ is bound in 
$\inC{k}{x}.P$. 
Binding for name and channel restriction is as usual.
Also, recursion variable $\rv{X}$ is bound in  process $\mu \rv{X}.P$.
%Based on these intuitions, g
Given a process $P$, its sets of free/bound channels, names, variables, and recursion variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fn}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bn}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are   as expected. 
In all cases, we rely on usual notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding) substitution.
The latter is noted $\subst{k}{x}$ (for channels) and $\subst{P}{\rv{X}}$ (for processes); 
we write $\subst{k_1, \ldots, k_n}{x_1, \ldots, x_n}$ to stand for an $n$-ary simultaneous substitution. 


Up to here, the language is a  synchronous $\pi$-calculi with sessions. 
Building upon 
\emph{locations} $\locf{loc}, \locf{l_1}, \locf{l_2}, \ldots$, 
%\emph{adaptation messages} (ranged over $r, r', \ldots$), 
novel process constructs are:
% the following: 
%\begin{enumerate}[-]
%\item 
\emph{located processes}, denoted $\scomponent{\locf{loc}}{P}$; 
%\item 
\emph{update processes}, denoted $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$; 
%\item runtime queues for channels and locations, denoted $ \que{\cha}{\ST} $ and $ \que{\locf{loc}}{\til{r}} $, respectively; 
%\item 
\emph{(session) monitors}, denoted $ \que{\cha^p}{\ST} $; 
%\item 
\emph{location queues}, denoted $ \que{\locf{loc}}{\til{r}} $; 
and
%\item 
\emph{adaptation  signals}, denoted $\outC{\locf{loc}}{r}$.
%\item 
Moreover, expressions include the 
\emph{arrive predicate}  $\arrive{\locf{loc}, r}$.

%\end{enumerate}
%while located processes have been central in our previous works~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}, constructs (b)--(d) above have been first introduced in~\cite{Kouzapas12}. As 
%we explain in detail next, here we adapt these constructs to the case of runtime adaptation (an issue not explored in~\cite{Kouzapas12}).
We now comment on each of these elements.
%As in~\cite{DBLP:conf/sac/GiustoP13,BGPZFMOODS}, given a process $P$ and a location $\locf{loc}$, 
%process $\scomponent{\locf{loc}}{P}$ denotes a \emph{located process}.
%Locations are transparent: inside \locf{loc}, process $P$ can freely evolve, possibly interacting with its environment. 
%They can be nested, which is particularly convenient when structuring processes for adaptability purposes.
\emph{Located processes} and 
\emph{update processes}
have been motivated in the Introduction.
Here we just limit to remark that 
update processes
are assumed to refer to at least one variable $x_i$ and to offer at least one alternative $Q_i$.
Also, 
process $\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$
is often abbreviated as 
$\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}$.
Update processes 
%the latter 
%\emph{Eventful update processes} rely on the current state of the session protocols running within a given location in order to determine an appropriate adaptation routine. For the sake of clarity, we illustrate first the particular case of \emph{diadic} eventful update processes (i.e., useful to adapt locations with at most two active sessions); then, we discuss the general $n$-adic case. 
%A diadic eventful update process is written as follows:
%\begin{equation}\label{eq:dya}
%\nadaptbig{\locf{loc}}{\mycase{x_1, x_2}{{x_{1}^{}{:}\ST_{1}^{i} \,;\,  x_{2}^{}{:}\ST_{2}^{i}}}{Q_i}{i \in {I}}}
%\end{equation}
%%Process~\eqref{eq:dya} 
%and 
%represents an adaptation routine for  sessions %$\cha_1^p, \cha_2^q$ located  at 
%enclosed by $\locf{loc}$. 
%As formalized by the operational semantics (see below),
%this process works  as a case operator on the session protocols currently associated to any channels $\cha_1^p, \cha_2^q$ in \locf{loc}:
%if such protocols ``match'' with one of the $\ST^j_1, \ST^j_2$ in the update process, then 
%the current behavior at \locf{loc} will be replaced with process $Q_j$.
%Otherwise, if no such match is possible, then the behavior at \locf{loc} is left unchanged and the update process at \locf{loc} is consumed. 
%Notice that a diadic update process  will be able to update \emph{at most} two sessions established at \locf{loc}. 
%This way, e.g., an update process such as~\eqref{eq:dya} could be defined to match only one session (say $\cha_1^p$). 
%%This way, for instance, if the current behavior at \locf{loc} involves exactly one running session, and the update process offers an alternative $Q_j$ which requires only a single matching option, then runtime adaptation will be possible.
%The general case for eventful update processes (given in (b) above) %is  in Table~\ref{tab:syntax}. It 
%generalizes \eqref{eq:dya} by 
%handling runtime adaptation for locations with at most $n$ running sessions.
%%\begin{equation}
%%\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}
%%\end{equation}
%Note that each option $i \in I$ may refer to a subset of the variables declared as $\til{x}$.
%Eventful update processes 
 generalize the $\mathtt{typecase}$ introduced in~\cite{Kouzapas12}, which defines a case-like choice based on a single channel;
 in contrast,  our update processes consider one or more channels.
%Note that we use dynamic session type inspection only for runtime adaptation purposes, while 
%in~\cite{Kouzapas12} 
%$\mathtt{typecase}$ is part of the syntax of processes. 
%This choice enables us 
%%to focus on  the key aspects of event-based concurrency that are key to runtime adaptation. Also, it allows us 
%%the limited use of our generalized form of $\mathtt{typecase}$ is also useful 
%to retain a standard session type syntax; see~\S\,\ref{s:types}. %simplify some parts of our technical development.

Update processes go hand-in-hand with \emph{monitors}, 
runtime entities which keep the current protocol state  at a given channel. 
We write $\que{\cha^p}{\ST}$ to denote the monitor which stores the protocol state $\ST$ for 
channel $\cha^p$. 
In~\cite{Kouzapas12}, a similar construct is used  as the queue that supports asynchronous communication. 
For simplicity, here we consider synchronous communication, and so monitors store  only the current protocol state. This choice is aligned with our goal of identifying the core elements from the eventful session framework that are central in enhancing runtime adaptation.
%\looseness=-1
%DA TOGLIERE: Extensions of our framework to the asynchronous case are discussed in Remark X.

\emph{Location queues}, not present in~\cite{Kouzapas12}, 
%are associated to locations; they 
handle adaptation requests (a sequence of messages $\til{r}$).
%they are denoted $\que{\locf{loc}}{\til{r}}$.
%Location queues 
They
enable us to give a unified treatment to adaptation requests, internal and external. 
The empty queue is denoted $\que{\locf{loc}}{\epsilon}$.
Given $\que{\locf{loc}}{\til{r}}$, it is worth observing that messages $\til{r}$ are not related to communication as abstracted by session types. This represents the fact that we handle adaptation requests and structured session exchanges as orthogonal issues. 
An \emph{adaptation signal} $\outC{\locf{loc}}{r}$ enqueues request $r$ into the location queue of $\locf{loc}$.
To this end, as detailed below, the operational semantics defines synchronizations between adaptation signals and location queues.
%
To connect  runtime adaptation and communication, our language allows the coupling of update processes with the \emph{arrive predicate on locations}, denoted \arrive{\locf{loc}, r}. %, which we now explain.
Inspired by the $\mathtt{arrive}$ predicate in~\cite{Kouzapas12}, this predicate detects if a  message $r$ 
%(which may represent a request for adaptation or upgrade) 
has been placed in the queue of  \locf{loc}. 

%Summing up, o
Our  language embodies several concerns related to runtime adaptation: using adaptation signals and location queues 
we may formally express
%\emph{who} may specify/trigger an adaptation event; by using queues  it also decrees 
\emph{how} an adaptation request is issued; the arrive predicate enables us to specify \emph{when} adaptation will be handled; using update processes and monitors we may specify \emph{what} is the goal of an adaptation event. 



%, noted $\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).


\begin{table}[t!]
\[
\begin{array}{lc}
 \rulename{r:Open} & 
\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \pired \hfill  \\
& \hfill 
\restr{\cha}{\big({\locc{P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST}}  \para  \locd{Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} }\big) } \quad (\ST \cdual \STT) \vspace{1.5mm} \\

\rulename{r:Com} &
\locc{\outCn{\overline{\cha}^{\,p}}{v}.P \para \que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\STT}}} 
\pired \hfill \\
&\hfill
\locc{P \para \que{\cha^p}{\ST}} \para  \locd{Q\sub{{v}\,}{{x}} \para \que{\cha^{\overline{p}}}{\STT} } \quad (\ST \cdual \STT) %\quad ({e} \downarrow {c}) 
\vspace{1.5mm}
\\
%\rulename{r:Sel} &
%C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} \para  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \} \para \\
%& D\{\select{\cha^{\,\overline{p}}}{n_j};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\overline{\ST_j} \}_{j \in J}}  \} 
%\pired \\
%& 
%\hfill C\{P_j \para \que{\cha^p}{\ST_j} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\overline{\ST_j}} \}  \quad (1 \leq j \leq m)  
\rulename{r:Sel} &
\locc{\branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J}\! \para\!  \que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}}}\! \para \!
\locd{\select{\cha^{\,\overline{p}}}{n_i};Q \para \que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}} } \\
& \hfill \pired   C\{P_i \para \que{\cha^p}{\ST_i} \}\para  D\{Q \para \que{\cha^{\overline{p}}}{\STT_i} \}  \quad (\ST_i \cdual \STT_i,\, i \in J)  
\vspace{1.5mm}
\\
\rulename{r:Clo} &
\locc{\close{\cha^{\,p}}.P \para \que{\cha^p}{\tend} } \para  \locd{\close{\cha^{\,\overline{p}}}.Q \para \que{\cha^{\overline{p}}}{\tend}} \pired %\\
%& \hfill 
\locc{P} \para  \locd{Q} \vspace{ 2mm}
\\
\rulename{r:Eva} & \text{if }e \pired e' \text{ then } \evc{E}[e] \pired \evc{E}[e']
\vspace{1.5mm}\\
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{1.5mm}
\\
%\rulename{r:Con} &  \text{if }P \pired P' \text{ then } \locc{P} \pired \locc{P'}
%\vspace{1.5mm}\\
%  \rulename{r:Loc} &
% \text{if } P \pired P'~~\text{then}~~ \scomponent{l}{P} \pired \scomponent{l}{P'} \vspace{1.5mm}
% \\ 
%\rulename{r:ResN} & \text{if }P \pired P' \text{ then } (\nu a)P \pired (\nu a)P'
%\vspace{1.5mm}\\
\rulename{r:ResC} &\text{if }P \pired P' \text{ then } (\nu \cha)P \pired (\nu \cha)P'
\vspace{1.5mm}\\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{1.5mm}
\\
 \rulename{r:Rec} &
\recu\,\rv X. P \pired P\subst{\recu\,\rv X. P }{\rv X}
\vspace{1.5mm}\\
\rulename{r:IfTrue} &
\ifte{\mathtt{true}}{P}{Q} \pired P    \vspace{1.5mm}
\\
% \rulename{r:IfFalse} &
%\ifte{\mathtt{false}}{P}{Q} \pired Q   \vspace{1.5mm}\\
\rulename{r:UReq} &  \locc{\que{\locf{loc}}{\til{r}_1}} \para \locd{\outC{\locf{loc}}{r}} \pired 
\locc{\que{\locf{loc}}{\til{r}_1 \cdot r}} \para \locd{\mathbf{0}}
\vspace{1.5mm}\\
\rulename{r:Arr} & \locc{\evc{E}[\arrive{\locf{loc},r}]} \para \locd{\que{\locf{loc}}{\til{r}}} \pired \locc{\evc{E}[\mathtt{b}]}
\para \locd{\que{\locf{loc}}{\til{r}}}  \  ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:UpdOld} & 
%\displaystyle\frac{
%\begin{array}{rcl} 
%\multicolumn{3}{c}{\mathsf{fc}(P)  = \cha_1^p, \ldots, \cha^p_n }
%%& &
%%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
%\\
% (V = P \land R' = R) & \bigvee  & \big(
% \mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) ~ \land~
%\\ 
%&& ~~~ V = Q_l\subst{\til{\cha}\,}{\,\til{x}_0} ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para\! \cdots\! \para \que{\cha^p_n}{\STT^{l}_n} 
%  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P \para R}} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V \para R'}} \para \locd{\mathbf{0}}
%\end{array}
%} 
%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{r:Upd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad \forall j \in [1,..,m]. (\Pin{P}{\que{\cha^p_j}{\ST_j}})}
%& &
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} 
\\
 (V = P) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
\\ 
&& \qquad V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m} 
  \big)
\end{array}
}{
\begin{array}{l}
\locc{\scomponent{\locf{loc}}{P}} \para
\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}}   
\pired \qquad \quad  \\
\hfill \locc{\scomponent{\locf{loc}}{V}} \para \locd{\mathbf{0}}
\end{array}
} 
%\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{r:Upd2} & 
%\displaystyle\frac{
%\begin{array}{c} 
%\mathsf{fc}(P) = \til{\cha} = \cha_1^p, \ldots, \cha^p_n \qquad
%R = \que{\cha^p_1}{\ST_1} \para \cdots \para \que{\cha^p_n}{\ST_n} \\
% (V = P \land R' = R)  ~~\bigvee~~  \\
%\exists \til{x}_0 \subseteq \til{x}, \rho .\big(
%|\til{k}| = |\til{x}_0| \land \til{x}_0 = \{x_1, \ldots, x_g\}  ~\land~ I' = \{u \in I \,|\, \mathsf{fc}(Q_u) = \til{x}_0\}~\land\\
% \exists l \in I'.(\forall j \in [1..n].\forall s \in [1..g].~~ \STT^{l}_s \leq \ST_j ~\land~  
%\forall r < l.\exists j \in [1..n].\exists s \in [1..g].~~\STT^{r}_s \not\leq \ST_j ~\land~ \\
%  \quad  
%\rho = \subst{\til{\cha}\,}{\,\til{x}_0} ~\land ~ V = \rho(Q_l) ~\land~
%R' = \que{\cha^p_1}{\STT_{1}^l} \para \cdots \para \que{\cha^p_n}{\STT^{l}_g} 
%)  \big)
%\end{array}
%}{
%\begin{array}{l}
%\locc{\scomponent{\locf{loc}}{P} \para R} \para
%\locdb{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m_i}^{}{:}\STT_{m_i}^{i}}}{Q_i}{i \in I}}}   
%\pired \qquad \\
%\hfill \locc{\scomponent{\locf{loc}}{V} \para R'} \para \locd{\mathbf{0}}
%\end{array}
%} 
\end{array}
%\vspace{-3mm}
\]
\caption{Reduction Semantics: Selected Rules.
Above, $\ST, \STT$ denote session types (cf. Def.~\ref{d:types})
\label{tab:redsem}}
\vspace{-7mm}
\end{table}
%\vspace{-3mm}

\paragraph{\textbf{Semantics.}}
The semantics of our process language is given by a \emph{reduction semantics},
the smallest relation generated by the rules in Table~\ref{tab:redsem}.
As usual, we write $P \pired P'$ for the reduction from $P$ to $P'$.
Reduction relies on 
%an evaluation relation on expressions, denoted $e \downarrow v$ (where $v$ is a value). Also, it uses 
a structural congruence, denoted $\equiv$ (see Definition~\ref{d:strcong}). %. (TO BE ADDED)
It also relies on  \emph{evaluation} and \emph{location} contexts:
\begin{eqnarray*}
\evc{E}  ::=  - \sepr \outC{k}{\evc{-}}.P \sepr  \ifte{\evc{-}}{P}{Q} \qquad \quad
C,D  ::=  - \sepr \scomponent{\locf{loc}}{C \para P}
\end{eqnarray*}
Given 
$\locc{\!\!-\!\!}$
 (resp. $\evc{E}[-]$), we write $\locc{P}$ (resp. $\evc{E}[e]$) to denote 
the process (resp. expression) obtained by filling in occurrences of hole $-$
in $C$ with $P$ (resp. in $\evc{E}$ with~$e$). 
%The extension of $\equiv$ to contexts is as expected.

%We comment on the rules . 
The first four rules in Table~\ref{tab:redsem} formalize session behavior within hierarchies of nested locations; they assume the expected duality over a polarity $p$, written $\overline{p}$. In rule~\rulename{r:Open} the synchronization on a name $u$ %with dual session types 
leads to the establishment of a session on fresh channels $\cha^p, \cha^{\overline{p}}$;
it also entails  the creation of two  monitors with the declared session type.
Such monitors are created in the same contexts in which the session is established. 
Hence, all monitors are \emph{local} by construction. 
Rule~\rulename{r:Com} represents  communication of a value: in addition to requiring complementary prefixes, we also require that the monitors support an input and output action. After reduction, prefixes in processes and monitors are consumed.  
This allows us to track the evolution of session protocols. Rule~\rulename{r:Sel} for labeled choice is standard, augmented with monitors. Rule~\rulename{r:Clo} formalizes coordinated session termination, discarding involved monitors.
%It is worth observing that we require that session queues are \emph{local} to the process. This way, for instance, a process 
%\begin{equation}
%\locc{\outCn{\overline{\cha}^{\,p}}{v}.P} \para \loccp{\que{\cha^p}{!(T).\ST} } \para \locd{\inC{\cha^{\,\overline{p}}}{{x}}.Q \para  \que{\cha^{\overline{p}}}{?(T).\overline{\ST}}} \nonumber
%\end{equation}
%is not able to reduce for the queue $ \cha^p$ is not local to the process executing that session.
The following six rules in the table define
standard and/or self-explanatory treatments for, respectively, reduction under evaluation contexts, parallel composition, located context, and restriction; applications of structural congruence; recursion and conditional operators
(with omitted rule~\rulename{r:IfFalse} being as expected).\looseness=-1 

The last three rules in Table~\ref{tab:redsem} define our event-based approach to runtime adaptation. 
Rule~\rulename{r:UReq} treats the issue of an adaptation request $r$ as a synchronization between a location queue and an adaptation signal. The queue and the signal may be in different  contexts;  this enables ``remote'' requests. Rule~\rulename{r:Arr} resolves arrive predicates within evaluation contexts
by querying the (possibly remote) queue. 
Rule~\rulename{r:Upd} defines the typeful update of the current protocol state at \locf{loc}, which is given 
by an indexed set of open sessions with their associated monitors.
%While at a first sight it may appear complex, the rule actually enforces a simple case operation over the running sessions at location \locf{loc}. The rule attempts to match (via subtyping, noted  $\csub$ in~\S\,\ref{s:types}) the current protocol state at \locf{loc} (embodied by the open sessions $\til{\cha}$ and their associated queues $R$) with the different options offered by the update process. The rule focuses on finding the first positive match; if no such 
%match exists then the current behavior at \locf{loc} ($P$, in the rule) is left unchanged, and the update process is consumed.\looseness=-1 
The rule attempts to match such protocol state with the first suitable option offered by an update process for \locf{loc}.
If there is no matching alternative the current protocol state at \locf{loc} is kept unchanged. %, and the update process is consumed.
By a slight abuse of notation, we write
$\Pin{P}{P_1}$ 
to indicate that $P_1$ occurs in $P$, i.e., 
if $P = C[P_1]$ for some  $C$.
Formally, 
given an index set $I$ over the update process, 
suitability with respect to the behavior at \locf{loc}
is defined 
by predicate $\mathsf{match}_I$ in Definition~\ref{d:matchp} below. 
Using subtyping $\csub$ (see \S\,\ref{s:types}), the predicate holds for an $l \in I$ which 
defines a new protocol state.

%\begin{definition}[Matching (Old)]\label{d:matchp}
%Given an index set $I$, session channels $\til{\cha}$, sets of variables $\til{x}$ and $\til{x}_0$,
%an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
%an indexed set of processes $\{Q_i\}_{i \in I}$, 
%and an  $l \in I$,
%we write 
%\begin{equation}
%\mathsf{match}_I(l,\, \til{\cha},\, \til{x} ,\,  \til{x}_0 ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I},\, \{Q_i\}_{i \in I}) \nonumber
%\end{equation}
%if and only if all of the following hold:
%\begin{enumerate}[(a)]
%\item $\til{x}_0 \subseteq \til{x} \land %\til{x}_0 = \{x_1, \ldots, x_g\} \land \til{\cha} = \{\cha^p_1, \ldots, \cha^p_n\} \land 
%|\til{x}_0| = |\til{\cha}| = n \land n \leq m$
%\item $\exists I' \subseteq I.(\forall h \in I'. \mathsf{fc}(Q_h) = \til{x}_0 \land l \in I')$
%\item $\forall r < l.\exists j \in [1..n].\exists s \in [1..n].~~\STT^{r}_s \not\csub \ST_j
%~~\land~~\forall j \in [1..n].\forall s \in [1..n].~~ \STT^{l}_s \csub \ST_j $
%\end{enumerate}
%\end{definition}
%Hence,  $\til{x}_0$ denotes a set of variables of the same cardinality of $\til{\cha}$ (condition (a)).
%Using $\til{x}_0$, condition (b) singles out the subset $I'$ of $I$ of suitable candidates for adaptation routines; index $l$ must be in $I'$. Condition (c) formalizes the fact that index $l$ refers to the first alternative to match, up to subtyping. 

\begin{definition}[Matching]\label{d:matchp}
Given an index set $I$, 
session types $\ST_1, \ldots, \ST_m$, 
an indexed sequence of session types $\{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}$, 
and an  $l \in I$,
we write 
\begin{equation*}
\mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) 
\end{equation*}
if and only if $\forall r < l.(\exists j \in [1..m].~\STT^{r}_j \not\csub \ST_j)
\land (\bigwedge_{h \in [1..m]} \STT^{l}_h \csub \ST_h)$.
\end{definition}
%Hence,  the matching predicate formalizes the fact that index $l$ refers to the first alternative that matches,  up to subtyping. 

%\noindent{\bf Example.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\input{example}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{example}
Recall process $W$ given in the Introduction. 
%\begin{equation}
%W  =   \scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ \nopenr{u}{x{:}\ST}.P^{50}} \para  \scomponentbig{\locf{seller}}{ \nopena{u}{y{:}\STT}.Q}\,} \nonumber
%\end{equation}
According to our semantics: % we have:
\begin{eqnarray*}
W & \pired& \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P_x^{50}\subst{\cha^p}{x} \para \que{\cha^p}{\ST}} \para  \scomponentbig{\locf{seller}}{Q_y\subst{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT}}\,} \big)}  \\ 
& \pired^2 & \restr{\cha}{\big(\scomponentbig{\locf{sys}}{\,\scomponentbig{\locf{buyer}}{ P_{\cha^p}' \para \que{\cha^p}{\ST_{\mathtt{pay}}}} \para  \scomponentbig{\locf{seller}}{Q_{\cha^{\overline{p}}}' \para \que{\cha^{\overline{p}}}{\STT_{\mathtt{pay}}}}\,} \big)} 
\end{eqnarray*}
Suppose that following an external request the seller must offer a new payment method (a gift card).
Precisely, we would like \pt{S} to act according to the following session type:
\begin{equation*}
\STT_{\mathtt{gift}} \,=\,\&\{\mathtt{addItem}:\, \&\{\mathtt{giftc}:\, \STT_\mathtt{gc} \,,\, \mathtt{ccard}:\, \STT_\mathtt{cc} \,,\, \mathtt{payp}:\, \STT_\mathtt{pp}\}\,,\,\mathtt{cancel}:\,\tend \} 
\end{equation*}
Let $\ST_{\mathtt{gift}}$ be the dual of $\STT_{\mathtt{gift}}$.
We then may define the following update process $R^1_{xy}$:
\begin{equation*}
{\nadaptbig{\locf{sys}}{\mycase{{x,y}}{x{:}\ST^{}_{\mathtt{pay}} \,;\, y{:}\STT^{}_{\mathtt{pay}}}{\scomponentbig{\locf{buyer}}{ P'_x \para \que{x}{\ST_{\mathtt{gift}}}} \para  \scomponentbig{\locf{seller}}{Q''_y \para \que{y}{\STT_{\mathtt{gift}}}}}{}}} 
\end{equation*}
Thus, $R^1_{xy}$ keeps the expected implementation for the buyer ($P'_x$), but updates its associated monitor.
For the seller, both the implementation and monitor are updated; above, $Q''_y$ stands for a process offering the three payment methods.
We may then specify the whole system as:
%\begin{equation}
$W \para \mu \rv{X}.\ifte{\arrive{\locf{sys}, \mathtt{upd}_E}}{R^1_{xy}}{\rv{X}}$.  
The type system introduced next  ensures that updates such as $R^1_{xy}$ consider both a process and its associated monitors, ruling out the possibility of discarding the monitors that enable reduction. Also, it ensures that behaviors added to a location such as \locf{sys} respect a declared \emph{interface}.
\end{example}

\section{Session Types for Eventful Runtime Adaptation}\label{s:types}
This section introduces a session type system for the process language of \S\,\ref{s:evadap}.
Our main result (Theorem~\ref{t:safety}) is that well-typed processes enjoy both \emph{safety} (absence of runtime communication errors)
and \emph{consistency} properties (update actions do not disrupt established sessions).
Our development follows the lines of the system in~\cite{GiustoP14}. 
\begin{definition}[Types]\label{d:types}
The syntax of \emph{basic types} (ranged over by $\capab, \sigma,   \ldots$) 
and \emph{session types} (ranged over by $\ST, \beta, \ldots$)
is given below. We use $T, S, \ldots$ to range over $\capab, \alpha$.
\[
\begin{array}{lclr}
%T, S&::=& \capab, \alpha \\
\capab, \sigma & ::= & \mathsf{name} \sepr \mathsf{bool}  ~~~& \text{basic types}\\

\alpha, \beta &::=  &  !(\capab).\alpha \sepr ?(\capab).\alpha  \sepr !(\beta).\alpha \sepr ?(\beta).\alpha  \quad& \text{send, receive, throw, catch} \vspace{0.5mm}\\ 
		& \sepr &  \&\{n_1{:}\alpha_1 \dots  n_m{:}\ST_m \} \sepr \oplus\{n_1{:}\alpha_1 \dots  n_m{:}\ST_m \}  &  \text{branch, select} \vspace{0.5mm} \\
		& \sepr &  \tend \!\!\!\!\!\!& \text{closed session} \vspace{0.5mm} \\
    & \sepr  & t \sepr  \mu t.\alpha & \text{type variable, recursion} 
\end{array}
\] %}
\end{definition}
%\noindent 
Although our process language copes with runtime adaptation, 
our type syntax is standard and retains the intuitive meaning of session types. 
Type $?({\capab}).\ST$ (resp. $?(\beta).\ST$) abstracts the behavior of a channel 
which receives a boolean or a session name (resp. a channel of type $\beta$) 
and then continues as $\ST$. 
Dually, type $!({\capab}).\ST$ (resp. $!(\beta).\ST$) represents the behavior
of a channel which sends a value (resp. a channel)  and then continues as $\ST$.
Type $\&\{n_1:\alpha_1 \dots  n_m:\ST_m \}$ describes a branching behavior:
it offers $m$ behaviors, and if the $j$-th alternative is selected then it behaves as described by type $\ST_j$ ($1 \leq j \leq m$).
In turn, type $\oplus\{n_1:\alpha_1 \dots  n_m:\ST_m \}$ describes the behavior of a channel which 
may select a single behavior among  $\alpha_1, \ldots, \alpha_m$ and then continues as $\ST_j$.
Type $\tend$ represents a channel with no communication behavior. Type $\mu t.\alpha$ describes recursive behavior;  
as usual, we consider recursive types under equi-recursive and contractive assumptions.

Following Gay and Hole~\cite{DBLP:journals/acta/GayH05}, 
we now introduce 
\emph{duality} and 
\emph{subtyping} over (session) types.
The former relies on a \emph{duality relation} (cf. Definition~\ref{def:dualr} in the Appendix);
the latter uses the  notion of \emph{type simulation} (given by Definition~\ref{def:simul} in the Appendix).

\begin{definition}\label{d:subt} Let $T, S$ be types.
\begin{enumerate}[$-$]
\item The \emph{coinductive duality relation}, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. 
\item The \emph{coinductive subtyping relation}, denoted \csub, is defined by $T \csub S$ if and only if there exists a type simulation $\mcc{R}$
such that $(T, S) \in \mcc{R}$. \\
The extension of $\csub$ to typings,  written $\ActS \csub \ActS'$, 
arises as expected.
\end{enumerate}
\end{definition}




Our typing judgments generalize usual notions with an  \emph{interface}~$\INT$.
Based on the syntactic occurrences of session establishment prefixes $\nopenr{a}{x{:}\ST}$, and $\nopena{a}{x{:}\ST}$,
the interface of a process describes the %(possibly persistent) 
services appearing in it.
Thus, intuitively, the interface of a process gives an ``upper bound'' on the services that it  may execute.
The typing system uses interfaces to control the behavior contained by locations after an update.
We have:


\begin{definition}[Interfaces]\label{d:interf}
We define an \emph{interface} as the multiset whose underlying set of elements 
$\mathrm{I}$ contains 
assignments from names to session types which are qualified.
More precisely: $\mathrm{I} = \{ \qua\,u{:}\ST ~|~ \qua \in \{\qual, \quau\}\}$, 
%\text{$u$ is a name, and $\ST$ is a session type}\}$$
We use $\INT, \INT', \ldots$ to range over interfaces.
We write $dom(\INT)$ to denote the set $\{u \mid u:\ST_\qua \in \INT \}$ and  $\#_\INT(a) = h$ to mean that element $a$ occurs $h$ times in $\INT$. 
\end{definition}
Thus, several occurrences of the same service declaration are captured by the multiset nature of interfaces.
The union of two interfaces $\INT_1$ and $\INT_2$ is essentially the union of their underlying multisets.
We sometimes write $\INT \addelta a:\ST_\qual$ 
and  $\INT \addelta a:\ST_\quau$
to stand 
for $\INT \addelta\{\qual\,a{:}\ST\}$ and 
$\INT \addelta \{\quau\,a{:}\ST\}$, respectively.
Moreover, we write $\INT_\qual$ (resp. $\INT_\quau$) to denote the subset of $\INT$ involving
only assignments qualified with $\qual$ (resp. $\quau$). 
We now define an ordering relation over interfaces, relying on subtyping:

%Next definition, extends the  subtyping relation to interfaces..

\begin{definition}[Interface Ordering] \label{d:rintpre}Given interfaces $\INT$ and $\INT'$, we write 
$\INT  \intpr \INT'$ iff 
\begin{enumerate}[1.]
\item $\forall (\qual\,a{:}\ST)$ such that  
 $\#_{\INT_\qual}(\qual\,a{:}\ST) = h$  with $h > 0$,
then  one of the following holds:
\begin{enumerate}[(a)]
\item there exists $h$ distinct elements $(\qual\,a{:}\STT_i) \in \INT'_\qual$ such that 
 $\ST \csub \STT_i$ for $ i \in [1..h]$;
\item there exists $(\quau\,a{:}\STT) \in \INT'_\quau$ such that  $\ST \csub \STT$.
\end{enumerate}
\item $\forall (\quau\,a{:}\ST) \in \INT_\quau $  then $ (\quau \, a{:}\STT) \in \INT'_\quau $ and $\ST \csub \STT$, for some $\STT$.
\end{enumerate}


\end{definition}


%\subsection{Environments, Judgments and Typing Rules}
% \begin{table}[t]
% \textsc{Environments}
% $$
% \begin{array}{lclr}
% 		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
% \ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
% \Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, a:\langle \ST_\qua , \overline{\ST}_\qua \rangle \quad& \text{first-order environment} \vspace{0.5mm} \\
% \Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,l:\INT     \quad& \text{higher-order environment}
% \end{array}
% $$  
% \caption{Types and Typing Environments. Interfaces $\INT$ are formally introduced in Definition~\ref{d:interf}.}\label{tab:types}
% \end{table}
% 

\begin{table}[t]
\[
\begin{array}{c}

\inferrule*[right=\rulename{t:LocEnv}]{ }{\typing{\Theta, \locf{loc}:\INT}{\locf{loc}}{\INT}} 
\quad \infer[\rulename{t:Que}]
 {\judgebis{\env{\Gamma}{\Theta}}{\que{k}{\ST}}{\type{k:\que{}{\ST}}{\emptyset}}}{}
\vspace{1.5mm} \\

\infer[\rulename{t:msg}]
{\typing{\Gamma}{r_1}{\msg}}{} \qquad

\infer[\rulename{t:locQ}]
{\typing{\Gamma}{r_1;\til{r}}{\msg}}
{\typing{\Gamma}{\til{r}}{\msg} & \typing{\Gamma}{r_1}{\msg}}\vspace{1.5mm} \\

\infer[\rulename{t:arrive}]
{\judgebis{\env{\Gamma}{\Theta}}{\arrive{\locf{loc}, r}}{\bool}}
{\typing{\Theta}{\locf{loc}}{\INT} \qquad\typing{\Gamma}{r}{\msg}} 
\qquad 
\infer[\rulename{t:Sig}]
{\judgebis{\env{\Gamma}{\Theta}}{\outC{\locf{loc}}{r}}{\type{\emptyset}{\emptyset}}}
{\typing{\Gamma}{r}{\msg}}
\vspace{1.5mm} \\


\inferrule*[right=\rulename{t:Loc} ]
 {
       \typing{\Theta}{\locf{loc}}{\INT} \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT' } }  \qquad \INT' \intpr \INT
 }{\judgebis{\env{\Gamma}{\Theta}}{\component{\locf{loc}}{}{\INT}{P} }{ \type{\ActS}{\INT' }}}
 \qquad
 \infer[\rulename{t:QLoc}]
{\judgebis{\env{\Gamma}{\Theta}}{\que{\locf{loc}}{\til{r}}}{\type{\emptyset}{\emptyset}}}
{ \typing{\Gamma}{\til{r}}{\msg}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Accept}]
{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \alpha \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Request}]
 {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \beta \qquad
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Clo}]
 {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Par}]
 {
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
 }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
\vspace{1.5mm} \\
\infer[\rulename{t:Adapt}]
{\judgebis{\env{\Gamma}{\Theta}}{\nadaptbig{\locf{loc}}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{j}; \cdots ;x_{m}^{}{:}\STT_{m}^{j}}}{Q_j}{j \in J}}}{\type{\emptyset}{\emptyset}}}
{\typing{\Theta}{\locf{loc}}{\INT} & \quad\forall j \in J, \ 
\judgebis{\env{\Gamma}{\Theta}}{Q_i}{\type{x_{1}{:}\mon{\STT_{1}^{j}}; \cdots ;x_{m}{:}\mon{\STT_{m}^{j}}}{\INT_j} } \qquad \INT_j \intpr \INT}
% \text{ where } \typeque{x:\STT} \text{ stands for } x:\STT, x:\que{}{\STT}
\vspace{1.5mm} \\
\infer[\rulename{t:RVar}]{\Gamma; \Theta,\rv X: \ActS, \INT \vdash \rv X:\type{\ActS}{\INT}}{}
\qquad
\infer[\rulename{t:Rec} ]{\judgebis{\env{\Gamma}{\Theta}}{\mu \rv X. P}{\type{\Delta}{\INT }}} 
{\judgebis{\env{\Gamma}{\Theta,\rv X: \type{\ActS}{\INT}}}{P}{\type{\Delta}{ \INT}} }
\vspace{1.5mm} \\
 
 \infer[\rulename{t:CRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS, \cha^p:\mon{\ST_1}, \cha^{\overline{p}}:\mon{\ST_2} }{ \INT}} & \ST_1 \cdual \ST_2} 

\vspace{1.5mm} \\

\infer[\!\!\rulename{t:Subs} ]{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS'}{\INT'}} } 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Delta}{ \INT}}& \ActS \csub \ActS' & \INT \intpr \INT'}
~~~
 \infer[\!\!\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
 {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
% \vspace{1.5mm} \\
% \infer[\rulename{t:NRes}]{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT}}}
% {\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS }{ \INT \cup \INT_u}} \quad  \ u \notin \dom{\INT} }
 %\text{ where } \INT_u \text{ contains only declarations for } u \ (i.e. \forall v\neq u, v\notin \dom{\INT_u} )
 \end{array}
 \]
\caption{Well-Typed Processes: Selected Rules} \label{tab:ts}
\vspace{-8mm}
\end{table}

\noindent We now define the typing environments on which our type system relies:
\[
\begin{array}{lclr}
		\qua & ::= &  \qual \sepr \quau  & \text{type qualifiers} \vspace{0.5mm} \\
\ActS & ::= &  \emptyset \sepr \ActS , k:\ST \sepr \ActS ,  k:\que{}{\ST}  & \text{typing with active sessions} \vspace{0.5mm} \\
\Gamma &::= &  \emptyset \sepr \Gamma, e:\capab \sepr \Gamma, u:\langle \ST_\qua , \STT_\qua \rangle \quad& \text{first-order environment (with $\ST_\qua \cdual \STT_\qua$)} \vspace{0.5mm} \\
\Theta &::= &  \emptyset \sepr  \Theta,\rv{X}:\type{\ActS}{\INT} \sepr \Theta,\locf{loc}:\INT     \quad& \text{higher-order environment}
\end{array}
\]  
In addition to interfaces $\INT$, we consider typings $\ActS$ and environments $\Gamma$ and $\Theta$. 
Typing $\ActS$  collects
assignments from channels to session types; as such, it describes
currently active sessions. 
In our discipline, 
$\ActS$ also includes \emph{bracketed assignments}, denoted $\kappa^p:\que{}{\ST}$,
which represent the type for monitors. 
Subtyping extends to these assignments: $\que{}{\ST} \csub \que{}{\STT}$ if  $\ST \csub \STT$.
We write $dom(\ActS)$ to denote the set $\{ k^p \mid k^p:\ST \in \ActS \lor k^p:\que{}{\ST} \in \ActS\}$. 
We write $\ActS , k:\ST $  where $k \not\in dom(\ActS)$.
Furthermore, we 
write $\ActS, k:\mon{\ST}$ to 
abbreviate $\ActS, k:\ST, k:\que{}{\ST}$.
That is, $k:\mon{\ST}$  describes both a session and its associated monitor.

$\Gamma$ is a first-order environment which maps expressions to basic types
and names to pairs of \emph{qualified} session types.
A session type is qualified with 
`$\quau$' if it is associated to a persistent service; otherwise, it is qualified with 
`$\qual$'. 
The higher-order environment $\Theta$ 
collects assignments of typings to process variables and interfaces to locations.
While the former concern recursive processes, the latter concerns located processes.
As we explain next, by relying on the combination of these two pieces of information the type system ensures that
runtime adaptation actions preserve the behavioral interfaces of a process.
We write $vdom(\Theta)= \{ \mathsf{X} \mid \mathsf{X}:\INT \in \Theta \}$ to denote the variables in the domain of $\Theta$.
Given these environments, a \emph{type judgment} is  of form\looseness=-1
\[\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}\] 
meaning that, under environments $\Gamma$ and $\Theta$, 
process $P$ has active sessions declared in $\ActS$ and interface 
$\INT$.
Some selected rules of the type system are shown in Table~\ref{tab:ts} (remaining rules can be found in Appendix \ref{ap:adtyping}).
Below we comment on some  of the rules: the rest are standard and/or self explanatory.
Rule \rulename{t:Adapt} types update processes. Notice that the typing rule that ensures each process $Q_i$ has exactly the same active sessions that those declared in the respective case.   
Also, we require that alternatives contain both processes and monitors. 
The requirement $\INT_j \intpr \INT$ guarantees that the process behavior does not ``exceed'' the expected behavior within the location.
Rule~\rulename{t:Subs} takes care of  subtyping both for typings $\ActS$ and interfaces. Rule~\rulename{t:CRes} types channel restriction that ensures typing duality among partners of a session and their respective queues.
Typing of queues is given by rule \rulename{t:Que} that simply assigns  type $k:\que{}{\ST}$ to queue $\que{k}{\ST}$.
Finally, rule \rulename{t:NRes} types hiding of service names, by simply removing their declarations from the interface $\INT$ of the process.
In the rule, 
$\INT_u$ contains only declarations for $u$, i.e., $\forall v\neq u, v\notin \dom{\INT_u}$.

\looseness=-1


Our type system enjoys the standard \emph{subject reduction} property. 
We rely on \emph{balanced} typings: $\ActS$ is balanced iff 
for all $\kappa^p:\ST \in \ActS$ (resp. $\kappa^p:\que{}{\ST} \in \ActS$)
then also 
$\kappa^{\overline{p}}: \STT \in \ActS$ (resp. $\kappa^{\overline{p}}: \que{}{\STT} \in \ActS$), with $\ST \cdual \STT$.
The proof, detailed in Appendix~\ref{app:proofs}, proceeds by induction on the last rule applied in the reduction; it adapts the one given in \cite{GiustoP14}.

\begin{theorem}[Subject Reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced and $P \pired Q$ then 
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS'}{\INT'}}$, for some $\INT'$ and balanced $\ActS'$.
\end{theorem}

We now define and state \emph{safety} and \emph{consistency} properties. 
While safety  guarantees  adherence to prescribed session types and absence of runtime errors, consistency ensures that sessions are not jeopardized by 
careless
%incautious 
 update actions.
Defining both properties requires the following notions of \emph{$\kappa$-processes}, \emph{$\kappa$-redexes}, 
and \emph{error process}.

\begin{definition}[$\kappa$-processes, $\kappa$-redexes, errors]\label{d:kred}
A process $P$ is a \emph{$\kappa$-process} if it is a prefixed process with subject $\kappa^p$, i.e., 
$P$ is one of the following:
\[
\begin{array}{lclcl}
    \inC{\kappa^{\,p}}{x}.P' & \qquad &  \outCn{\overline{\kappa}^{\,p}}{v}.P' & \qquad &     \close{\kappa^{\,p}}.P'    \\
   \branch{\kappa^{\,p}}{n_i{:}P_i}_{i \in I}  &  \quad&   \select{\kappa^{\,p}}{n}.P'  & \quad& 
\end{array}
\]
Process $P$ is a \emph{$\kappa$-redex} if 
it contains the composition of exactly two $\kappa$-processes with opposing polarities.
$P$ is an \emph{error} if
$P \equiv (\nu \til{\kappa})(Q \para R)$
where, for some $\kappa$, $Q$ contains 
\underline{either} 
exactly 
two $\kappa$-processes that do not form a $\kappa$-redex
\underline{or}
three or more $\kappa$-processes.
\end{definition}


Informally, a process $P$
is called \emph{consistent} 
if whenever  it has a $\kappa$-redex  then  update actions do not destroy such a redex.  Below, we formalize this intuition. 
Let us write $P \pired_{\text{upd}} P'$ 
for any reduction inferred using rule $\rulename{r:Upd}$. We then define:

\begin{definition}[Safety, Consistency]\label{d:consis}
Let $P$ be a process.
We say $P$ is \emph{safe} if it never reduces into an error. 
We say $P$ is \emph{update-consistent} 
if and only if,
 for all $P'$ and $\kappa$ 
such that $P \pired^{*} P'$ and $P'$ contains a $\kappa$-redex, 
if $P' \pired_{\text{upd}} P''$
then $P''$ contains a $\kappa$-redex.
\end{definition}


We now state our main result; it follows as a  consequence of Theorem~\ref{th:subred}.
 
\begin{theorem}[Typing Ensures Safety and Consistency]\label{t:safety}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}}$ with $\ActS$ balanced
then $P$ is update consistent and %never reduces into an error.
safe.
\end{theorem}


%\input{types.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Discussion: A Compartmentalized Model of  Communication and Adaptation}\label{s:arch}
\newcommand{\myapp}[4]{#1\big\langle #2 \,;\, #3\,;\, #4\big\rangle }
\newcommand{\stpar}{\diamond}
\newcommand{\appar}{\parallel}
\newcommand{\mapar}{\circ}

%As discussed  in \S\,\ref{s:evadap}, 
%the novel mechanisms for runtime adaptation present in our process language operate at the level of locations.
%The introduction of located processes and mechanisms for runtime adaptation defined over locations 
%We now address the following 
%This raises a 
%natural question: 
Given that 
the process model in \S\,\ref{s:evadap}
describes the interplay of both communication and adaptation concerns, 
how should specifications be organized in order to 
reflect a desirable separation of concerns?
%achieve modular treatment of runtime adaptation? 
Here
we propose to organize specifications using \emph{compartments} which 
isolate 
communication behavior and adaptation routines.
%Here we propose an adaptation-oriented model for communicating processes.

Our model offers an alternative for specifying systems at a high-level of abstraction.
It defines \emph{systems} % are deployed 
in a two-level scheme: from a global perspective, a system 
%(ranged over by $G, G', \ldots$)
is the composition of \emph{applications}.
%, denoted $A_1, A_2, \ldots$. 
%local to each application, we have (located) processes %(as introduced above) 
%with their runtime state.
%As we will see, some degree of communication between applications will be allowed.
%Each application has a unique identifier, denoted $a_1, a_2, \ldots$.
There are  \emph{handler} processes, %denoted $\mathcal{H}_1, \mathcal{H}_2,  \ldots $, 
which are responsible for adaptation at the 
system (global) level:  a handler may 
update a location at some specific application or 
upgrade a service definition.
%Also, there is an initialization process $\mathsf{Init}$ which starts the system by appropriately invoking applications.
%Up to this point, we have:
%\begin{eqnarray}
%Sys & = &  A_1 \appar \cdots \appar A_n \appar \mathcal{H}_1 \appar \cdots \appar \mathcal{H}_k  \nonumber 
%\end{eqnarray}
%where `$\appar$' denotes the parallel composition operator at the system level. 
Applications comprise three   elements: 
\emph{behavior}, \emph{state}, and a \emph{manager}.
While the first 
concerns session processes, the second comprises monitors and location queues.
%contains located service definitions and invocations, the second stores monitors and location queues associated to the behavior of the application, together with a queue for the application. 
Managers %denoted $\mathcal{M}_1, \mathcal{M}_2,  \ldots $, 
implement adaptation policies at the application (local) level. %This scheme thus realizes the desired separation of concerns.
As we wish to isolate communication behavior from adaptation routines, 
the presence of update processes is confined to handlers and managers.

%Let us define the syntax of our architecture:
%\begin{eqnarray*}
%Sys & = & A_1 \parallel \cdots \parallel A_n \parallel \mathcal{H} \parallel  \mathsf{Init} \\
%A_i& = & id\langle R \,, S\, , \mathcal{M} \rangle \\
%R & ::= & \scomponent{\locf{loc}}{!a(x).P}   \sepr \scomponent{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
%S & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}}
%\end{eqnarray*}
%\subsubsection*{Definition.} 

Our model of compartmentalized communication is defined %by the syntax 
in Table~\ref{t:model}.
The process syntax that we use in this section  
is a subset of that introduced in Table~\ref{tab:syntax}: 
\begin{eqnarray*}
P , Q & ::=  &   \nopenr{u@a}{x:\ST}.P  \sepr   \nopena{u}{x:\ST}.P  \sepr   \outC{\locf{loc}@a}{r}   \\
& \sepr &   \outC{k}{e}.P  \sepr   \inC{k}{x}.P
	\sepr   \select{k}{n};P  
   \sepr   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} 
    \sepr   \close{k}.P   \\
   & \sepr &  \mu \rv{X}.P  
	\sepr   \rv{X} 
  	\sepr   \ifte{e}{P}{Q}  
  	\sepr    P \para  P  	 
		\sepr    \restr{\cha}{P}   
	 \sepr   \restr{a}{P}   
	 \sepr   \mathbf{0}   
\end{eqnarray*}
Our set of processes 
is thus comparable to most session $\pi$-calculi, only extended with the (possibly remote) adaptation request $\outC{\locf{loc}@a}{r}$, which refers to location \locf{loc} in application $a$.
%We write $\prod_{j \in [1..m]} P_j$ to denote the process $P_1 \para \cdots \para P_m$.
Similarly, our notation for session requests refers to a service $u$ at application $a$.
%The need for reference will become clear later on. 
%Let us assume the following abbreviations:
We shall write $\ast\ift{e}{P}$ 
to stand for $\mu \rv{X}.\ifte{e}{P}{\rv{X}}$, 
and $\repopen{u}{x{:}\ST}.P$ to stand for $\mu \rv{X}.\nopena{u}{x{:}\ST}.(P \para \rv{X})$. 
%\begin{eqnarray}
%\ast\ift{cond}{P} & \triangleq & \mu \rv{X}.\ifte{cond}{P}{\rv{X}} \nonumber \\
%\repopen{u}{x{:}\ST}.P & \triangleq & \mu \rv{X}.\nopena{u}{x{:}\ST}.(P \para \rv{X})  \nonumber
%\end{eqnarray}
Also, we write $P^{-}$ to denote the sublanguage of processes without service definitions $\nopena{u}{x{:}\ST}.P$.
%As it will be clear later on, this is useful to isolate service definitions. 

\begin{table}[!t]
\begin{eqnarray*}
G & ::= & A \sepr \mathcal{H} \sepr \restr{\cha}{A} \sepr G_1 \appar G_2 \sepr \mathbf{0} \qquad \quad
A  :: =  \myapp{a}{R}{\mathsf{S}}{\mathcal{M}} \\
%g & :: = & \arrive{\locf{l}@a, \mathtt{upd}_E} \sepr g_1 \land g_2 \sepr g_1 \lor g_2\\
\mathcal{H} & ::= & 
*\,\ift{\arrive{\locf{l}_1@a, \mathtt{upd}_E}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \\
& \sepr & *\,\ift{\arrive{\locf{l}_1@a, \mathtt{upg}}}{\nupgbig{\locf{l}_1}{P}} 
\\
R & ::= & \scomponentbig{\locf{loc}}{\nopena{u}{x{:}\ST}.P}   \sepr  \scomponentbig{\locf{loc}}{\repopen{u}{x{:}\ST}.P}   \sepr \scomponentbig{\locf{loc}}{P^{-}}  \sepr R_1 \para R_2 \\
\mathsf{S} & ::= & \que{\cha^p}{\ST} \sepr \que{\locf{loc}}{\til{r}} %\sepr \que{a}{\til{r}}  
\sepr \mathsf{S}_1 \stpar \mathsf{S}_2 \sepr \mathbf{0} \\
\mathcal{M} & ::= & *\,\ift{\arrive{\locf{l}_1, \mathtt{upd}_I}}{\nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}}} \sepr  \mathcal{M}_1 \mapar \mathcal{M}_2   \sepr \mathbf{0}
%& \sepr & \mathcal{M}_1 \para \mathcal{M}_2 
\end{eqnarray*}
%\vspace{-3mm}
\caption{A Compartmentalized Model of Communicating Systems: Syntax\label{t:model}}
\vspace{-8mm}
\end{table}


%Recall that $\locf{loc}, \locf{l}_1, \locf{l}_2, \ldots$ range over locations. 
%We write $G, G_1, G_2, \ldots$ to denote elements at the global (system) level. 
A system $G$ is the composition of finite sets of  
applications $A$ and handlers $\mathcal{H}$; this composition is denoted $\parallel$.
Given $A_i = \myapp{a_i}{R_i}{\mathsf{S}_i}{\mathcal{M}_i}$, we refer to $a_i$ as the name of $A_i$.
A handler is a persistent process which 
spawns an adaptation strategy as soon as a  request arrives to an appropriate queue. 
%Notice this is the only part of our model where update processes may occur. 
Handlers may either  $\mathtt{upd}$ate 
or  $\mathtt{upg}$rade
the behavior at some location $\locf{loc}$ within application $a$; this is written $\locf{loc}@a$.
Upgrades are
denoted $\nupgbig{\locf{l}_1}{P}$; they are a particular form of update 
intended for service definitions only. 
% included within an application. 
%They may also 
%As mentioned above, applications are a compartment for communicating behaviors, 
%their associated state, and related adaptation policies. % are jointly described. 
%Indeed, the structure of applications enforces a separation between behavior and state, but also  a separation with respect to adaptation policies. 
We use $R$ to denote the communication behavior of an application. %, enclosed within locations: 
As before, locations are transparent; for simplicity, here we rule out their nesting. 
%A design criteria in the specification of $R$ is the 
We distinguish  between located processes representing service definitions 
from the located processes which make use of such definitions.
Our operational semantics (motivated below) ensures that locations enclosing service definitions do not contain open (active) sessions. 
This may be convenient for organizing adaptation strategies, since updates to service definitions may now be performed without concerns of disruption of active sessions. The state $\mathsf{S}$ of an application collects
session monitors and location queues.
 %the queues associated to the behavior contained: we consider queues for sessions and locations (as before) 
% but also a queue for the application, denoted $\que{a}{\til{r}}$. 
A manager $\mathcal{M}$ is  meant to react upon the arrival of an internal adaptation message $\mathtt{upd}_I$. 
 We use $\mathsf{S}_1 \stpar \mathsf{S}_2$ 
 and $\mathcal{M}_1 \mapar \mathcal{M}_2$ 
 to denote the composition of $\mathsf{S}_1$ and $\mathsf{S}_2$ and $\mathcal{M}_1$ and $\mathcal{M}_2$, respectively.
Appendix~\ref{app:examcm} illustrates the use of compartments in the buyer-seller example.
%In fact, it is worth noticing that managers may act upon the issue of an internal update request $\mathtt{upd}_I$ for some location, whereas handlers may act upon the arrival of an external update request or an application upgrade request (denoted $\mathtt{upd}_E$ and $\mathtt{upg}$, respectively).

Even if the syntax in Table~\ref{t:model} already induces useful structuring principles for systems, 
we find it desirable to give the following \emph{well-formedness conditions}. 
%This is the content of the below definition.
Recall that we write $\Pin{P}{P_1}$ if $P_1$ occurs in $P$.
%\begin{definition}\label{d:wfsys}
%Given the syntax in Table~\ref{t:model}, 
%we will say that $G$ is a \emph{well-formed system} if it satisfies the following conditions:
%\begin{enumerate}[1.]
%\item 
First, all applications in $G$ should have pairwise distinct names.
%\item 
Second, for each $\Pin{G}{\myapp{a_i}{R_i}{\mathsf{S}_i}{\mathcal{M}_i}}$, we have:
%\begin{enumerate}[(a)]
%\item 
(a)~Processes in $\mathcal{M}_i$ only refer to locations occurring in $R_i$.
%\item 
(b)~For each location $\locf{loc}_j$ occurring in $R_i$ there is exactly one queue $\Pin{\mathsf{S}_i}{\que{\locf{loc}_j}{\til{r}}}$.
%\end{enumerate}
%\end{enumerate}
%\end{definition}
We now %informally 
comment on %some key rules of the 
the
reduction semantics for well-formed systems.
%In particular, w
We illustrate how such a semantics builds upon 
the principles embodied by the semantics for  ``plain'' processes (cf. \S\,\ref{s:evadap}) but propagating the structural organization introduced above. A full account of the reduction semantics is in Appendix~\ref{app:commodel}.

%We first comment on rules for session establishment. 
Our semantics 
%The first rule 
enables \emph{remote session establishment} in which a request for service $u$ in application $a_2$ is served by a definition in application $a_1$ (below we assume $\ST \cdual \STT$):
\begin{equation*} 
\begin{array}{c}
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\nopena{u}{x{:}\ST}.P \para R}}{\mathsf{S}_1}{\mathcal{M}_1} \appar  
\myapp{a_2}{\scomponentbig{\locf{l}_2}{\,\nopenr{u@a_1}{y{:}\STT}.Q}}{\mathsf{S}_2}{\mathcal{M}_2} \vspace{-0.5mm}
  \spired   \vspace{1mm}\\
 \restr{\cha}{\big(\myapp{a_1}{\scomponentbig{\locf{l}_1}{R}}{\mathsf{S}_1}{\mathcal{M}_1} \appar 
 %\qquad \qquad \qquad \qquad \qquad \qquad 
 \hfill \myapp{a_2}{\scomponentbig{\locf{l}_2}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}{
\mathsf{S}_2 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\STT}
}{\mathcal{M}_2}\big)} 
\end{array} 
\end{equation*}
\begin{table}[t]
\begin{equation*}
\displaystyle\rulename{c:LUpd}\,\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad 
\mathsf{S} \equiv \mathsf{S}_1 \stpar \que{\cha^p_1}{\ST_1} \stpar \cdots \stpar \que{\cha^p_m}{\ST_m} \stpar \mathsf{S}_2}
\\
 (V = P \land \mathsf{S}' = \mathsf{S}) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
\\ 
&& \qquad V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m}  ~ \land~
\\
&& \qquad \mathsf{S}' = \mathsf{S}_1 \stpar \que{\cha^p_1}{\STT_1} \stpar \cdots \stpar \que{\cha^p_m}{\STT_m} \stpar \mathsf{S}_2
  \big)
\end{array}
}{
\begin{array}{l}
 \myapp{a}{\scomponentbig{\locf{l}_1}{P} \para R}{
\mathsf{S} 
}{\mathcal{M} \para \nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}} }  
 \spired \qquad \quad  \\
\hfill \myapp{a}{\scomponentbig{\locf{l}_1}{V} \para R}{
\mathsf{S}' 
}{\mathcal{M} \para \mathbf{0} }  
\end{array}
} 
\end{equation*}
\caption{Reduction Rule for Managers in the Compartmentalized Model\label{f:updcm}}
\vspace{-8mm}
\end{table}
Above, it is worth observing how the instance of the service is deployed at the caller location (denoted $\locf{l}_2$).
Since we would like to impose a certain degree of isolation between applications, this will be the only rule admitted at the application level. Local session establishment takes place between services and clients inside a certain application $a$:
%Session establishment within applications is of course allowed:
\begin{equation*} 
\begin{array}{c}
\myapp{a}{\scomponentbig{\locf{l}_1}{\nopena{u}{x{:}\ST}.P \para R} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\STT}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} \spired  \qquad \qquad \qquad \qquad \qquad \qquad \hfill \vspace{1mm}\\
 \restr{\cha}{\big( \myapp{a}{\scomponentbig{\locf{l}_1}{R} \para \scomponentbig{\locf{l}_2}{ P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y}}}{
\mathsf{S}_1 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\STT}
}{\mathcal{M}_1}\big)} 
\end{array} 
\end{equation*}
%As in the remote rule, h
Here again the instantiated service ``moves'' from $\locf{l}_1$ to $\locf{l}_2$.
%The reduction rule for session communication rule is then defined as 
%\begin{equation} \nonumber
%\begin{array}{c}
% \myapp{a}{\scomponentbig{\locf{l}_1}{\outCn{\cha^{\,p}}{v}.P \para \inC{\cha^{\,\overline{p}}}{{x}}.Q }}{
%\mathsf{S} \stpar 
%\que{\cha^p}{!(T).\ST} \stpar
%\que{\cha^{\overline{p}}}{?(T).\STT} 
%}{\mathcal{M}}  \spired \vspace{1mm}\\
% \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q\subst{v}{x} }}{
%\mathsf{S} \stpar 
%\que{\cha^p}{\ST} \stpar \que{\cha^{\overline{p}}}{\STT} 
%}{\mathcal{M}} 
%\end{array}
%\end{equation}
%Rules for choice and session closure follow similar lines.
%Conditionals and arrival predicates are handled as in the semantics of \S\,\ref{s:evadap}.
Let us consider rules for adaptation.
At the application level, the semantics of managers relies on rule~\rulename{c:LUpd}, given in Table~\ref{f:updcm}.
Such a rule strictly refines  rule~\rulename{r:Upd} in Table~\ref{tab:redsem}.
Observe how having the state $\mathsf{S}$ allows us to precisely specify the elements that have influence on (and are modified by)
dynamic reconfiguration. 
At the level of systems, the semantics of handlers is given by two rules: one for update (similar to the rule above)
and the following rule for 
service upgrade:  %of a service definition: %at the global level:
\begin{equation*}
\myapp{a}{\scomponentbig{\locf{l}_1}{P} \para R}{
\mathsf{S} 
}{\mathcal{M} }  \appar \nupgbig{\locf{l}_1}{Q}
 \spired
 \myapp{a}{\scomponentbig{\locf{l}_1}{Q} \para R}{
\mathsf{S} 
}{\mathcal{M}  }  \appar \mathbf{0} 
 \end{equation*}
Our model induces specifications in %of interacting systems in 
which requirements of communication, runtime adaptation, and state (as useful in, e.g., asynchronous communication) are jointly expressed, while keeping a desirable separation of concerns.
%It is worth noticing that 
Notice that
the differences between %the syntax and semantics of 
``plain'' processes 
(as given in \S\,\ref{s:evadap}) and %those for 
well-formed systems are mostly conceptual, rather than technical. 
In fact, the higher level of abstraction that is enforced by well-formed systems does not result in additional technicalities.
Although our compartmentalized model builds upon plain processes, we conjecture that a reduction-preserving translation of application-based specifications into processes does not exist---a main difficulty being, unsurprisingly, properly representing the separation between behavior and state. 
This difference in terms of expressiveness does not appear to affect the type system. 
%In fact, w
We are confident that the typing discipline developed in \S\,\ref{s:types} (and its associated guarantees)  extend to well-formed systems without major technical difficulties. 
We plan to address this conjecture in future work.
%For instance, typing the upgrades is simple using interfaces

%To substantiate this claim, we now show how systems the high-level compartmentalized model may be translated into the plain processes of \S\,\ref{s:evadap}.
%\begin{definition}
%Let $G$ be a well-formed system, in the sense of Definition~\ref{d:wfsys}. The translation $\encp{\cdot}{}$ from systems to plain processes is given as follows:
%\[
%\begin{array}{rclcrcl}
%\encp{G_1 \parallel G_2}{} & = & \encp{G_1}{} \para  \encp{G_2}{} & \quad & 
%\encp{\myapp{a}{R}{\mathsf{S}}{\mathcal{M}}}{} & = & \scomponentbig{\locf{a}}{\, \encp{R}{a} \para \encp{\mathsf{S}}{a} \para \encp{\mathcal{M}}{a}} \vspace{1mm}\\
%\encp{{R_1 \para R_2}}{a} & = & \encp{R_1}{a} \para \encp{R_2}{a} & & \encp{\scomponent{\locf{loc}}{\repopen{u}{x{:}\ST}.P}}{a} & = & \scomponentbig{\locf{loc}}{\repopen{u_a}{x{:}\ST}.\encp{P}{a}} \vspace{1mm}\\
%\encp{{\mathsf{S}_1 \stpar \mathsf{S}_2}}{a} & = & \encp{\mathsf{S}_1}{a} \para \encp{\mathsf{S}_2}{a} & & \encp{\scomponent{\locf{loc}}{\nopenr{u@a_1}{x{:}\ST}.P}}{a} & = & \scomponentbig{\locf{loc}}{\nopenr{u_{a_1}}{x{:}\ST}.\encp{P}{a}} 
%%\encp{\scomponent{\locf{loc}}{P}}{a} & = & \scomponentbig{\locf{loc}}{\encp{P}{a}} 
% \end{array}
%\]
%and where $\encp{\cdot}{}$  and  $\encp{\cdot}{a}$
%are isomorphisms for the remaining constructs.
%\end{definition}
%Using $\encp{\cdot}{}$, we may reuse the results in the previous sections to reason about communication safety and update consistency 
%of systems in the compartmentalized model. Minor modifications are required. First, let us write $\spired$ for the reduction relation 
%generated by the rules in Table~\ref{tab:redsem} except for rule~$\rulename{r:Open}$, which is replaced with the following rule:
%\[
%\begin{array}{lc}
% \rulename{r:RemOpen} & 
%\locc{\nopena{u}{x:\ST}.P} \para  \locd{\nopenr{u}{y:\STT}.Q} \spired \hfill   \\
%& \qquad 
%{ {\locc{\mathbf{0}}  \para  \locd{\restr{\cha}\big( P\sub{\cha^{p}}{x} \para \que{\cha^p}{\ST} \para Q\sub{\cha^{\overline{p}}}{y} \para \que{\cha^{\overline{p}}}{\STT} \big)} } }
%~~~ (\ST \cdual \STT) 
%\end{array}
%\]
%The main properties of well-typed processes (safety, consistency) can be shown to hold for the modified reduction $\spired$.
%This enables us to lift reasoning techniques from low-level plain processes to the higher level of abstraction represented by well-formed systems in the compartmentalized model.
%%We are therefore confident that the typing system of \S\,\ref{s:types} can be easily extended to systems,
%%including  guarantees of safety and consistency by typing.
%
%




\section{Related Work and Concluding Remarks}\label{s:concl}

\paragraph{\textbf{Related Work.}}
%\noindent\emph{\textbf{Related Work.}~}
%The closest related work is the PhD thesis of Kouzapas~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}, which introduces event-bases processes for asynchronous communication together with a complete framework to test arrival of messages and test types of queues. As mentioned throughout the paper we have been inspired by this machinery but we have considerably changed the domain and scope of application. 
% 
The combination of static typing and type-directed tests for dynamic reconfiguration is not new.
For instance, Seco and Caires~\cite{DBLP:conf/esop/SecoC06} formalize this combination for a calculus for object-oriented component programming.
To the best of our knowledge, ours is the first framework to develop this combination for a session process language.
As discussed along the paper, the most related works are by Kouzapas et al.~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11,KouzapasJ13,Kouzapas12}. The earliest works on eventful sessions, including theory and implementation aspects, are~\cite{DBLP:conf/ecoop/HuKPYH10,DBLP:conf/forte/KouzapasYH11}. %; an associated journal paper is~\cite{KouzapasJ13}. %We have often referred to 
Kouzapas's PhD thesis~\cite{Kouzapas12} provides a  unified presentation of the eventful framework, with case studies including  event selectors (a building block in event-driven systems) and transformations between multithreaded and event-driven programs.  
%Besides the eventful process constructs, 
At the level of types, 
the work in~\cite{KouzapasJ13,Kouzapas12} introduces session set types to support the $\mathtt{typecase}$ construct. 
%Since our typecase construct is embedded inside update processes, our type system may rely on a standard session type syntax.
Note that we use dynamic session type inspection only for runtime adaptation purposes;  %, while 
in~\cite{Kouzapas12} 
$\mathtt{typecase}$ is part of the process syntax. 
This choice enables us 
to retain a standard session type syntax. %; see~\S\,\ref{s:types}. 
%As mentioned above, r
Runtime adaptation of session communication---the novel contribution of this paper---seems to be an  application of  eventful session types not previously identified.
 We refer to~\cite{GiustoP14} for %detailed 
 comparisons with related works on runtime adaptation and (binary, multiparty) session types. 

\paragraph{\textbf{Concluding Remarks.}} 
%\noindent\emph{\textbf{Concluding Remarks.}~} 
We have introduced an event-based approach to runtime adaptation of session typed processes. 
We identified the strictly necessary eventful process constructs that enhance and refine known
mechanisms for runtime adaptation. 
Adaptation requests, both internal and external, are uniformly treated via event detectors and queues associated to locations. 
This eventful approach to adaptation enables us to 
specify rich forms of updates on locations with running sessions; this represents a concrete improvement with respect to our previous work~\cite{GiustoP14}, in which typeful updates are only allowed when locations do not enclose running sessions.
We notice that expressing both internal and external exceptional events is useful in practice; 
for instance, both kinds of events coexist in  
%the Business Process Model \& Notation (BPMN) 
BPMN 2.0~(see, e.g.,~\cite[Chap.4]{DBLP:books/daglib/0031128}).
We also introduced a type system that ensures communication safety and update consistency. 
To further motivate the significance of our typed framework, we have outlined 
a high-level  model of structured interaction which builds upon ``plain'' processes and 
organizes their main communication and adaptation components into a sensible structure. 

In future work we plan to further validate the constructs in our framework.
For instance,  
we plan to use the eventful constructs proposed here to enhance the model of \emph{supervision trees} (a mechanism for fault-tolerance in Erlang)
that we gave in~\cite{DBLP:journals/corr/GiustoP13}.
% we gave a model of supervision trees which relied on the adaptation mechanisms put forward in our previous work~\cite{GiustoP14}).
Our developments are kept purposefully simple, and admit several extensions. 
% two of them are 
%, thus, believe that by slightly modifying the present proposal  we can adapt our framework to i) describe 
For instance, an extension with
\emph{asynchronous} communication 
would rely on the machinery in~\cite{Kouzapas12}, 
 %already defines the required machinery, which could be incorporated in our framework by 
 using monitors to record both the current session type and in-transit messages.
%Also, it could be useful to explore an extension with \emph{higher-order} runtime adaptation, in which 
%location queues are refined in such a way that 
%in addition to an adaptation signal, they also receive from the environment a process defining an adaptation routine.
%In the first case, the framework proposed by Kouzapas et al. can be adopted here by simply enriching the information on channel  queues.  The second enhancement can be obtained for instance by allowing location queues to receive together with the adaptation signal an update routine to be executed on the locality. 
Also, well-formed systems %of the compartmentalized model % approach can be followed for architectures where states and managers 
could be %refined so as to handle also faults and communication problems. This can be achieved 
enhanced with memories storing not only the current state but also some previous history, thus  allowing  
a session to \emph{rollback} to a previous state. 
Another  interesting topic %that we plan to address is 
would be  
%our approach 
to accommodate %global protocols 
choreographic protocols
via multiparty session types~\cite{DBLP:conf/popl/HondaYC08}. 
We expect that well-formed systems would play a key role in defining the endpoint projections of choreographies described by 
(global)
types.
%SEE JOURNAL FOR DISCISSION ON ADAPTATION FOR SESSION TYPES

\vspace{-2mm}

{\small
\bibliographystyle{abbrv}
\bibliography{referen}
}
\newpage

\appendix
\section{An Example of the Compartmentalized Model}\label{app:examcm}
\input{examplecompartment}
\section{Supplementary Definitions} \label{app:types}
\subsection{Structural Congruence}
\begin{definition}[Structural Congruence]\label{d:strcong}
Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:


$$
\begin{array}{cc}
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\newname}{\nil} \!\equiv\! \nil & \restr{\newname}{\restr{\newname'}{P}} \!\equiv\! \restr{\newname'}{\restr{\newname}{P}} \\
\restr{\newname}{P} \!\para \! Q \!\equiv\! \restr{\newname}{(P \!\para \! Q)} ~~\text{(if $\newname \not\in \mathsf{fc}(Q) \cup \mathsf{fn}(Q) $)} \qquad &
\restr{\newname}{\component{\locf{loc}}{}{\Delta}{P}} \!\equiv\! \component{\locf{loc}}{}{\Delta}{\restr{\newname}{P}}  


% \restr{\kappa}{\nil} \!\equiv\! \nil & \restr{\kappa}{\restr{\kappa'}{P}} \!\equiv\! \restr{\kappa'}{\restr{\kappa}{P}} \\
% \restr{\kappa}{P} \!\para \! Q \!\equiv\! \restr{\kappa}{(P \!\para \! Q)} ~~\text{(if $\kappa \not\in \mathsf{fc}(Q)$)} \qquad &
% \restr{\kappa}{\component{\locf{loc}}{}{\Delta}{P}} \!\equiv\! \component{\locf{loc}}{}{\Delta}{\restr{\kappa}{P}}  \\
% \restr{u}{\nil} \!\equiv\! \nil & \restr{u}{\restr{u'}{P}} \!\equiv\! \restr{u'}{\restr{u}{P}} \\
% \restr{u}{P} \!\para \! Q \!\equiv\! \restr{u}{(P \!\para \! Q)} ~~\text{(if $u \not\in \mathsf{fn}(Q)$)} \qquad &
% \restr{u}{\component{\locf{loc}}{}{\Delta}{P}} \!\equiv\! \component{\locf{loc}}{}{\Delta}{\restr{u}{P}} \\
% \multicolumn{2}{l}{\nadaptbig{\locf{loc}}{\mycase{x_1, \ldots, x_m}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}} \equiv} \\
% \multicolumn{2}{r}{\qquad \qquad\nadaptbig{\locf{loc}}{\mycase{x_{\sigma(1)}, \ldots, x_{\sigma(m)}}{{x_{\sigma(1)}{:}\STT_{1}^{i}; \cdots ;x_{\sigma(m)}{:}\STT_{\sigma(m)}^{i}}}{Q_i}{i \in I}}}
\end{array}
$$
with $\newname, \newname',\ldots$ ranges over both names and session channels.
%where $\sigma$ stands for a permutation of  $\{1, \ldots, m\}$.
The extension of $\equiv$ to contexts is as expected.
\end{definition}

\subsection{Coinductive Subtyping and Duality}
For all types, define $\unf{T}$ by recursion on the structure of $T$:
$$\unf{\mu t.T} = \unf{T\subst{\mu t.T}{t}}$$ 
and $\unf{T} = T$ otherwise.
The following definition is used by Definition~\ref{d:subt}.
Given an index set $I = \{1, \ldots, m\}$, we use 
$\&\{n_i:\ty_i\}_{i \in I}$ 
and 
$\oplus\{n_i:\ty_i\}_{i \in I}$ 
to abbreviate 
$\&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ 
and 
$\oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$, respectively.

\begin{definition}\label{def:dualr}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{duality relation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\tau \csub \sigma$ and  $\sigma \csub  \tau$.

\item If $\unf{\ty} = \tend$ then $\unf{\tyy} = \tend$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = !(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $\ty_2 \csub \tyy_2$ and $\tyy_2 \csub \ty_2$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\ty_1, \tyy_1) \in \mcc{R}$ and  $\tau_i \csub \sigma_i$ and  $\sigma_i \csub  \tau_i$.

\item If $\unf{\ty} = \&\{n_1:\ty_1 \dots  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1 \dots  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \oplus\{n_1:\ty_1 \dots  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1 \dots  n_m:\tyy_m \}$ and
for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\end{enumerate}

% \end{definition}
% 
% We may now define:
% 
% \begin{definition}
%The \emph{coinductive duality relation}, denoted \cdual, is defined by $T \cdual S$ if and only if there exists a duality relation $\mcc{R}$
%such that $(T, S) \in \mcc{R}$. 
\end{definition}

\begin{definition}\label{def:simul}
A relation $\mathcal{R} \subseteq \mathcal{T} \times \mathcal{T}$ is a \emph{type simulation}
if $(\ty, \tyy) \in \mathcal{R}$ implies the following conditions:
\begin{enumerate}[1.]
\item If $\unf{\ty} = \capab$ then $\unf{\tyy} = \sigma$ and $\capab \bsub \sigma$.

\item If $\unf{\ty} = \tend$ then $\unf{\tyy} = \tend$.

\item If $\unf{\ty} = ?(\ty_2).\ty_1$ then $\unf{\tyy} = ?(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\ty_2, \tyy_2)  \in \mcc{R}$.

\item If $\unf{\ty} = \,!(\ty_2).\ty_1$ then $\unf{\tyy} = \,!(\tyy_2).\tyy_1$ and $(\ty_1, \tyy_1) \in \mcc{R}$ \\ and  $(\tyy_2, \ty_2)  \in \mcc{R}$.

\item If $\unf{\ty} = ?(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = ?(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\tau_i, \sigma_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.

\item If $\unf{\ty} = !(\tau_1, \ldots, \tau_n).\ty_1$ then $\unf{\tyy} = !(\sigma_1, \ldots, \sigma_n).\tyy_1$ then
for all $i \in [1..n]$, we have that $(\sigma_i, \tau_i) \in \mcc{R}$ and $(\ty_1, \tyy_1) \in \mcc{R}$.




\item If $\unf{\ty} = \oplus\{n_i:\ty_i\}_{i \in I}$ then $\unf{\tyy} = \oplus\{n_j:\tyy_j\}_{j \in J}$ 
and $I \subseteq J$ for all $i \in I$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

%\item If $\unf{\ty} = \oplus\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \oplus\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
%and $m \leq h$ for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.

\item If $\unf{\ty} = \&\{n_i:\ty_i\}_{i \in I}$ then $\unf{\tyy} = \&\{n_j:\tyy_k\}_{j \in J}$ 
and $J \subseteq I$ for all $j \in J$, we have that $(\ty_j, \tyy_j) \in \mcc{R}$.


%\item If $\unf{\ty} = \&\{n_1:\ty_1, \dots,  n_m:\ty_m \}$ then $\unf{\tyy} = \&\{n_1:\tyy_1, \dots,  n_h:\tyy_h \}$ 
%and $h \leq m$ for all $i \in [1..m]$, we have that $(\ty_i, \tyy_i) \in \mcc{R}$.



\end{enumerate}
\end{definition}



\subsection{Additional Typing Rules}\label{ap:adtyping}
Table \ref{t:addtyperules} gives additional typing rules for the system in \S\,\ref{s:types}.

\begin{table}[!t]
{\small
$$
\begin{array}{c}
% \mathrm{\textsc{Comp}}~~~\component{a}{P} \arro{~\component{a}{P}~}  \star
\infer[\rulename{t:bool}]
{\typing{\Gamma}{\true, \false}{\bool}}{} 
\qquad
\infer[\rulename{t:name}]
{\typing{\Gamma}{u}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:bVar}]
{\typing{\Gamma, x: \bool }{x}{\bool}}{} 
\qquad
\infer[\rulename{t:nVar}]
{\typing{\Gamma, x: \name}{x}{\name}}{} 
\vspace{1.5mm} \\
\infer[\rulename{t:eq}]
{\typing{\Gamma}{d=d}{\bool}}{d=u \vee d=\kappa^p \vee d =x} \qquad 
\infer[\rulename{t:Ser}]
{\typing{\Gamma, u:\langle\ST_\qua, {\STT}_\qua\rangle}{u}{\langle\ST_\qua, {\STT}_\qua\rangle}}{\ST \cdual \STT } 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Nil}]{ }{\judgebis{\env{\Gamma}{\Theta}}{\nil}{\type{\emptyset}{\emptyset}}}
\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Accept}]
%{\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qual , {\STT}_\qual  \rangle} \quad \gamma \csub \alpha \qquad \judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma}{\,\INT}}}{  \judgebis{\env{\Gamma}{\Theta}}{\nopena{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: \gamma_\qual}}}
%\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Request}]
% {\ST \cdual \STT \quad \typing{\Gamma}{u}{\langle \ST_\qua , {\STT}_\qual \rangle} \quad \gamma \csub \beta \qquad
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, x:\gamma }{\,\INT}} 
%}{\judgebis{\env{\Gamma}{\Theta}}{ \nopenr{u}{x:\gamma}.P}{ \type{\ActS}{\,\INT \addelta u: {\gamma}_\qual }}} 
%\vspace{1.5mm} \\
%\inferrule*[right=\rulename{t:Clo}]
% {\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\ActS}{\INT}} \quad k\notin \dom{\ActS} }{\judgebis{\env{\Gamma}{\Theta}}{ \close{k}.P}{ \type{\ActS, k:\tend}{ \INT}}}
%\quad
%\inferrule*[right=\rulename{t:Par}]
% {
%\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS_1}{ \INT_1}} \quad
% \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\ActS_2}{ \INT_2}}
% }{\judgebis{\env{\Gamma}{\Theta}}{P \para Q}{\type{\ActS_1 \cup \ActS_2}{\INT_1 \addelta \INT_2}}}
%
%\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Thr}] 
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT}{ \INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{k'}.P}{\type{\ActS, k:!(\ST).\STT, k':\ST}{ \INT}}}
\quad
\inferrule*[right=\rulename{t:Cat}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\STT, x:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{x}.P }{\type{\ActS, k:?(\ST).\STT}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:In}]
{\judgebis{\env{\Gamma, {x}:{\capab}}{\Theta}}{P}{\type{\ActS, k:\ST}{\INT}}}{\judgebis{\env{\Gamma}{\Theta}}{\inC{k}{{x}}.P }{\type{\ActS, k:?({\capab}).\ST}{ \INT}}}
\quad 
\inferrule*[right=\rulename{t:Out}]
{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST}{ \INT}} \quad \typing{\Gamma}{e}{\capab}}
{\judgebis{\env{\Gamma}{\Theta}}{\outC{k}{{e}}.P}{\type{\ActS, k:!({\capab}).\ST}{ \INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Weakc}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad \cha^+, \cha^- \notin dom(\ActS)}{\judgebis{\env{\Gamma}{\Theta}} {\restr{\cha}{P}}{\type{\ActS}{ \INT }}}
 
\quad
\inferrule*[right=\rulename{t:Weakn}] 
{\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\ActS}{ \INT}  } \quad u \notin dom(\INT)}
{\judgebis{\env{\Gamma}{\Theta}} {\restr{u}{P}}{\type{\ActS}{ \INT }}}


\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:If}]
 {
 \typing{\env{\Gamma}{\Theta}}{ e}{\mathsf{bool}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\ActS}{\INT}} \qquad 
\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\ActS}{\INT}}
 }{\judgebis{\env{\Gamma}{\Theta}}{\ifte{e}{P}{Q}}{\type{\ActS}{\INT}}} 
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Bra}] 
{
\judgebis{\env{\Gamma}{\Theta}}{P_1}{\type{\ActS, k:\ST_1}{ \INT_1}} 
\quad 
\cdots
\quad
\judgebis{\env{\Gamma}{\Theta}}{P_m}{\type{\ActS, k:\ST_m}{ \INT_m}} \quad \INT = \INT_1 \uplus ...\uplus \INT_m
 }{\judgebis{\env{\Gamma}{\Theta}}{\branch{k}{n_1{:}P_1 \alte \cdots \alte  n_m{:}P_m}}{\type{ \ActS, k:\&\{n_1{:}\ST_1, \ldots, n_m{:}\ST_m \}}{\INT}}}
\vspace{1.5mm} \\
\inferrule*[right=\rulename{t:Sel}]
{
\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\ActS, k:\ST_i}{ \INT}} \qquad 1 \leq i \leq m 
}{\judgebis{\env{\Gamma}{\Theta}}{\select{k}{n_i};P}{\type{\ActS, k:\oplus\{n_1:\ST_1, \ldots,  n_m:\ST_m \}}{\INT}}}
\end{array}
$$
}
\caption{Additional Typing Rules\label{t:addtyperules}}
\end{table}

\subsection{Reduction Semantics for the Compartmentalized Model}\label{app:commodel}
See  Tables~\ref{tab:redsemari} and~\ref{tab:redsemarii} for reduction for systems $G$, denoted $\spired$.
For all entities (processes, managers, applications, etc.) we assume 
a structural congruence relation $\equiv$ that validates the usual properties for
their associated parallel composition operator, with neutral element $\mathbf{0}$.
Similarly as process reduction,  $\spired$ relies on an evaluation relation on expressions, denoted $e \downarrow v$ (where $v$ is a value).
Also, it relies on the  definition of \emph{evaluation contexts} $\evc{E}[-]$ given before.
Furthermore, we assume a rule 
\rulename{c:GUpd2}
which is very similar to \rulename{c:LUpd}.
\begin{table}[t!]
$$
\begin{array}{lc}
\rulename{c:ROpen} & 
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\nopena{u}{x{:}\ST}.P \para R}}{\mathsf{S}_1}{\mathcal{M}_1} \appar  
\myapp{a_2}{\scomponentbig{\locf{l}_2}{\,\nopenr{u@a_1}{y{:}\STT}.Q}}{\mathsf{S}_2}{\mathcal{M}_2} \vspace{-0.5mm}\\
&  \spired   \vspace{-0.5mm}\\
& \restr{\cha}{\big(\myapp{a_1}{\scomponentbig{\locf{l}_1}{R}}{\mathsf{S}_1}{\mathcal{M}_1} \appar \\
& \myapp{a_2}{\scomponentbig{\locf{l}_2}{( P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y})}}{
\mathsf{S}_2 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\STT}
}{\mathcal{M}_2}\big)} \vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:LOpen} & 
\myapp{a_1}{\scomponentbig{\locf{l}_1}{\nopena{u}{x:\ST}.P \para R} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\STT}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} \vspace{-0.5mm}\\
& \spired   \vspace{-0.5mm}\\
& %\hfill 
 \restr{\cha}{\big( \myapp{a_1}{\scomponentbig{\locf{l}_1}{R} \para \scomponentbig{\locf{l}_2}{ P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y}}}{
\mathsf{S}_1 \stpar 
\que{\cha^+}{\ST} \stpar 
\que{\cha^{-}}{\STT}
}{\mathcal{M}_1}\big)} \vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\rulename{c:LOpen!} & 
%\myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{\nopenr{u}{y:\STT}.Q}}{\mathsf{S}_1}{\mathcal{M}_1} \vspace{-0.5mm}\\
%& \spired   \vspace{-0.5mm}\\
%& 
%\restr{\cha}{\big( \myapp{a_1}{\scomponentbig{\locf{l}_1}{\repopen{u}{x:\ST}.P} \para \scomponentbig{\locf{l}_2}{  P\sub{\cha^+}{x} \para Q\sub{\cha^-}{y}}}{
%\mathsf{S} \stpar 
%\que{\cha^+}{\ST} \stpar 
%\que{\cha^{-}}{\STT}
%}{\mathcal{M}}\big)} 
%\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Com} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{\outCn{\cha^{\,p}}{v}.P \para \inC{\cha^{\,\overline{p}}}{{x}}.Q }}{
\mathsf{S} \stpar 
\que{\cha^p}{!(T).\ST} \stpar
\que{\cha^{\overline{p}}}{?(T).\STT} 
}{\mathcal{M}}  \vspace{-0.5mm}\\
& \spired \vspace{-0.5mm}\\
& 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q\subst{v}{x} }}{
\mathsf{S} \stpar 
\que{\cha^p}{\ST} \stpar \que{\cha^{\overline{p}}}{\STT} 
}{\mathcal{M}}  
\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Sel} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{ \branch{\cha^{\,p}}{n_j{:}P_j}_{j \in J} \para  \select{\cha^{\,\overline{p}}}{n_j};Q   }}{
\mathsf{S} \stpar 
\que{\cha^p}{\&\{n_j{:}\ST_j\}_{j \in J}} \stpar
\que{\cha^{\overline{p}}}{\oplus\{n_j:\STT_j \}_{j \in J}}
}{\mathcal{M}}  \vspace{-0.5mm} \\
& \spired \vspace{-0.5mm}\\
& 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P_j \para Q}}{
\mathsf{S} \stpar 
\que{\cha^p}{\ST_j} \stpar \
\que{\cha^{\overline{p}}}{\STT_j} 
}{\mathcal{M}}  \quad (j \in J)  
\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:Clo} &
 \myapp{a}{\scomponentbig{\locf{l}_1}{\close{\cha^{\,p}}.P    \para  
 \close{\cha^{\,\overline{p}}}.Q  }}{
\mathsf{S} \stpar 
\que{\cha^p}{\tend} \stpar
\que{\cha^{\overline{p}}}{\tend}
}{\mathcal{M}}  
 \spired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P \para Q}}{
\mathsf{S}  
}{\mathcal{M}}   
\vspace{4mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:LUpd} & 
\displaystyle\frac{
\begin{array}{rcl} 
\multicolumn{3}{c}{\mathsf{fc}(P) = \{ \cha_1^p, \ldots, \cha^p_m \} \qquad 
\mathsf{S} \equiv \mathsf{S}_1 \stpar \que{\cha^p_1}{\ST_1} \stpar \cdots \stpar \que{\cha^p_m}{\ST_m} \stpar \mathsf{S}_2}
\\
 (V = P \land \mathsf{S}' = \mathsf{S}) & \bigvee  & \exists l.\big(
 \mathsf{match}_I(l,\, \{\ST_1, \ldots, \ST_m\} ,\, \{\STT_1^i, \ldots, \STT_m^i\}_{i \in I}) ~ \land~
\\ 
&& \qquad V = Q_{l\,}\subst{\cha^p_1, \ldots, \cha^p_m\,}{\,x_1, \ldots, x_m}  ~ \land~
\\
&& \qquad \mathsf{S}' = \mathsf{S}_1 \stpar \que{\cha^p_1}{\STT_1} \stpar \cdots \stpar \que{\cha^p_m}{\STT_m} \stpar \mathsf{S}_2
  \big)
\end{array}
}{
\begin{array}{l}
 \myapp{a}{\scomponentbig{\locf{l}_1}{P} \para R}{
\mathsf{S} 
}{\mathcal{M} \para \nadaptbig{\locf{l}_1}{\mycase{\til{x}}{{x_{1}^{}{:}\STT_{1}^{i}; \cdots ;x_{m}^{}{:}\STT_{m}^{i}}}{Q_i}{i \in I}} }  
 \spired \qquad \quad  \\
\hfill \myapp{a}{\scomponentbig{\locf{l}_1}{V} \para R}{
\mathsf{S}' 
}{\mathcal{M} \para \mathbf{0} }  
\end{array}
} 
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\rulename{c:GUpd1} & 
\displaystyle\frac{
\mathsf{fc}(P) = \emptyset 
}{
 \myapp{a}{\scomponentbig{\locf{l}_1}{P} \para R}{
\mathsf{S} 
}{\mathcal{M} }  \appar \nupgbig{\locf{l}_1}{Q}
 \spired
 \myapp{a}{\scomponentbig{\locf{l}_1}{Q} \para R}{
\mathsf{S} 
}{\mathcal{M}  }  \appar \mathbf{0}

} 
\end{array}
$$
\caption{Selected Reduction Rules for Compartmentalized Processes (I). We assume $\ST \cdual \STT$. \label{tab:redsemari}}
\end{table}

\begin{table}[t!]
$$
\begin{array}{c}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GCRes}]{A \spired A'}{ \restr{\cha}{A} \spired\restr{\cha}{A'}
}
\qquad 
\inferrule[\rulename{c:LCRes}]{R \spired R'}{ \restr{\newname}{R} \spired\restr{\newname}{R'}
}
   \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:Str}]{}{
\text{if } P \equiv P',\, P' \spired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \spired Q }
\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:Rec}]{}{ 
\recu\,\rv X. P \spired P\subst{\recu\,\rv X. P }{\rv X}}
   \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:IfTrue}]{}{ 
\ifte{\mathtt{true}}{P}{Q} \spired P}    
%   \vspace{2mm}\\
\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \inferrule[\rulename{c:IfFalse}]{}{\ifte{\mathtt{false}}{P}{Q} \spired Q }
   \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LPar1}]{P \spired P'}{ \myapp{a}{\scomponentbig{\locf{l}_1}{P \para R_1} \para R_2 }{
\mathsf{S}  
}{\mathcal{M}} \spired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{P' \para R_1} \para R_2 }{
\mathsf{S}  
}{\mathcal{M}}
}
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LPar2}]{\mathcal{M} \spired \mathcal{M}'}{ \myapp{a}{R}{
\mathsf{S}  
}{\mathcal{M} \mapar \mathcal{M}_1} \spired 
 \myapp{a}{R}{
\mathsf{S}  
}{\mathcal{M}' \mapar \mathcal{M}_1}
}
%\vspace{2mm}\\
\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GPar1}]{G \spired G'}{G \appar G_1 \spired G' \appar G_1}  
\vspace{2mm}\\
%\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[ \rulename{c:Rec}]{}{ \recu\,\rv X. P \spired P\subst{\recu\,\rv X. P }{\rv X}}
%%\vspace{2mm}\\
%\qquad
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[\rulename{c:IfTr}]{}{\ifte{\mathtt{true}}{P}{Q} \spired P }
%\vspace{2mm}\\
%%\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:UReq1}]{}{
 \myapp{a}{\scomponentbig{\locf{l}_1}{~\outC{\locf{loc}@a}{r} \para R }}{
\mathsf{S} \stpar \que{\locf{loc}}{\til{r}_1} 
}{\mathcal{M}} \spired 
 \myapp{a}{\scomponentbig{\locf{l}_1}{ R }}{
\mathsf{S} \stpar \que{\locf{loc}}{\til{r}_1 \cdot r} 
}{\mathcal{M}}}
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:UReq2}]{}{
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{~\outC{\locf{loc}@a_2}{r} \para R }}{
\mathsf{S}_1  
}{\mathcal{M}_1} 
\appar
 \myapp{a_2}{R_2}{
\mathsf{S}_2 \stpar \que{\locf{loc}}{\til{r}_1} 
}{\mathcal{M}_2} 
\spired \\
 \myapp{a_1}{\scomponentbig{\locf{l}_1}{R }}{
\mathsf{S}_1  
}{\mathcal{M}_1} 
\appar
 \myapp{a_2}{R_2}{
\mathsf{S}_2 \stpar \que{\locf{loc}}{\til{r}_1 \cdot r} 
}{\mathcal{M}_2} }
\vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[\rulename{c:GUpd1}]{}{\myapp{a}{R}{\mathsf{S}  }{\mathcal{M}} \appar \nadaptbig{a}{ \myapp{a}{R'}{\mathsf{S}'  }{\mathcal{M}'}} \spired \myapp{a}{R'}{\mathsf{S}'}{\mathcal{M}'} }
% \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[\rulename{c:GUpd2}]{}{\myapp{a}{\scomponentbig{\locf{loc}}{P} \para R }{
%\mathsf{S}  
%}{\mathcal{M}} \appar \nadaptbig{\locf{loc}}{Q} \spired
%\myapp{a}{\scomponentbig{\locf{loc}}{Q} \para R }{\mathsf{S}  }{\mathcal{M}} }
% \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\inferrule[\rulename{c:GArr1}]{}{\myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\arrive{a,r}]  \spired \myapp{a}{R}{\mathsf{S} \stpar \que{a}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\mathtt{b}] }
% \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
% \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:GArr}]{}{ \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\arrive{\locf{loc}@a,r}]  \spired \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M}} \appar \evc{E}[\mathtt{b}] }
 \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
 \vspace{2mm}\\
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\inferrule[\rulename{c:LArr}]{}{  \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M} \para \evc{E}[\arrive{\locf{loc},r}]}   \spired \myapp{a}{R}{\mathsf{S} \stpar \que{\locf{loc}}{\til{r}}  }{\mathcal{M} \para \evc{E}[\mathtt{b}] } }
 \quad ((|\til{r}| \geq 1) \downarrow \mathtt{b}) 
\end{array}
$$
\caption{Selected Reduction Rules for Compartmentalized Processes (II).\label{tab:redsemarii}}
\end{table}


\section{Omitted Proofs}\label{app:proofs}
\input{proof}


\end{document}

The report should contain the following information:
- purpose of the STSM;
- description of the work carried out during the STSM;
- description of the main results obtained;
- future collaboration with host institution (if applicable);
- foreseen publications/articles resulting or to result from the STSM (if applicable);
- confirmation by the host institution of the successful execution of the STSM;
- other comments (if any).


